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.

  • 5
    $\begingroup$ 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. $\endgroup$ May 19, 2013 at 11:26
  • 3
    $\begingroup$ 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. $\endgroup$ May 19, 2013 at 11:30
  • $\begingroup$ Ah, I see why I was confused. Thanks. $\endgroup$
    – Dabs
    May 19, 2013 at 12:25
  • 3
    $\begingroup$ 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$. $\endgroup$ May 19, 2013 at 17:27

1 Answer 1


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.

  • $\begingroup$ I see, thanks. Simpson's statements are true regardless (see comments above). $\endgroup$
    – Dabs
    May 19, 2013 at 12:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.