Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
5  
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
2  
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
1  
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
add comment

1 Answer

up vote 6 down vote accepted

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.

share|improve this answer
    
I see, thanks. Simpson's statements are true regardless (see comments above). –  Dabs May 19 '13 at 12:28
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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