Let $A$ be a recursive set. $A$ is recursively enumerable, so $A$ may be defined by a $\Sigma^0\_1$ formula, i.e. by $\exists \overrightarrow{a} \phi (\overrightarrow{a}, n)$, where $\phi$ contains no quantifiers (Matiyasevich's theorem). The complement of $A$ is r.e. so $A$ may be defined by a $\Pi^0\_1$ formula $\forall \overrightarrow{a} \psi (\overrightarrow{a}, n)$. Is there a result guaranteeing that the equivalence (true in $\mathbb{N}$)
$\forall n (\exists \overrightarrow{a} \phi (\overrightarrow{a}, n) \leftrightarrow \forall \overrightarrow{a} \psi (\overrightarrow{a}, n))$ is provable, say, in Peano's arithmetic ? 




---


The reason I ask is the following. Simpson (in *Subsystems of second-order Arithmetic*), following Friedman, defines a subsystem of second-order arithmetic, $\textbf{RCA}\_0$, with, as restricted comprehension axiom scheme, the universal closure of
$\forall n ( \phi(n) \leftrightarrow \psi(n) ) \rightarrow \exists X \forall n (n\in X \leftrightarrow \phi (n) )$
for $\phi$ any $\Sigma^0\_1$ formula and $\psi$ any $\Pi^0\_1$ formula. So any set this axiom guarantees the existence of will be recursive (or recursive in some other sets if $\phi$ happens to contain free set variables). My problem is that Simpson seems to assume the converse (see eg p. 64) : that this axiom scheme postulates the existence of all recursive sets. But, as far as I can tell, this requires that the equivalence above be provable in his system for appropriate $\phi$ and $\psi$, and I don't see how to prove this. 



Is the equivalence between a $\Sigma^0_1$ and a $\Pi^0_1$ formula defining the same recursive set provable in a sufficiently strong arithmetic ?
No, in general, a true $\Delta^0\_1$ assertion may not necessarily be provably $\Delta^0\_1$ in a given theory. For example, assume $\text{Con}(\text{PA})$ is true, and consider the formula $\phi(a)$ asserting that $a=a$ and the formula $\psi(a)$ asserting that "$a$ is not the code of a proof of a contradiction in $\text{PA}$," which is expressible as saying that $a$ does not solve a certain specific diophantine equation. 


Since we assumed there is no such proof, we have that $\exists a\ \psi(a)$ is equivalent to $\forall a\ \psi(a)$, since these are both true sentences. But there can be no proof of this equivalence in $\text{PA}$, if it is consistent, since $\text{PA}$ proves the former sentence, but if it were to prove the latter sentence, it would be proving its own consistency. 


