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.

provethat $(\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$. $\endgroup$ – Carl Mummert May 19 '13 at 17:27