# 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 ?

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.

-
The equivalence doesn't need to be provable; it just needs to be true. And as you note, the equivalence is true in every $\omega$-model, so every $\omega$-model of RCA$_0$ contains all recursive sets. –  Dan Turetsky May 19 '13 at 11:26
To add a little more, Simpson's statement isn't occurring within RCA$_0$. Rather, he's reasoning in the metatheory. In the metatheory, we can conclude that any model of RCA$_0$ contains all recursive sets. –  Dan Turetsky May 19 '13 at 11:30
Ah, I see why I was confused. Thanks. –  Dabs May 19 '13 at 12:25
This is one of those situations where it would be possible to replace an axiom with a weaker rule of inference. We could consider a comprehension rule of inference which says that when we prove that $(\forall n)[\phi(n) \leftrightarrow \psi(n)]$ then we can assert the existence of $\{n : \phi(n)\}$. That would give a significantly weaker theory than $\mathsf{RCA}_0$. –  Carl Mummert May 19 '13 at 17:27

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.