# Formula $\Sigma_{1}$ in $Q$ but not $\Sigma_{1}$

A formula $\varphi$ is $\Sigma_{1}$ over a given theory $T$ if $T\vdash \varphi \leftrightarrow \psi$ for some $\psi \in \Sigma_{1}$.

Is there a formula $\varphi$ in the language of arithmetic that is $\Sigma_{1}$ over (Robinson's) $Q$ but not $\Sigma_{1}$? What about one that is $\Sigma_{1}$ over $Th(\mathbb{N})$ but not over $Q$? Please provide examples, if possible.

-
I removed the tags 'arithmetic', 'model theory', 'computability', and 'incompleteness', and added 'proof theory'. The tag wiki for 'arithmetic' shows it is intended for elementary things, and the others didn't seem like good fits. –  Carl Mummert Jul 24 '11 at 23:26
@CarlMummert: I don't think this is a proof-theory question. –  Kaveh Jul 24 '11 at 23:43
@Kaveh: It's somewhat common, at least in computability-influenced settings, to classify this sort of thing as proof theory. It's not ordinal analysis, but it is the study of provability in formal theories. As a side note, I would deeply appreciate it if you typed the space in my name. –  Carl Mummert Jul 25 '11 at 1:05
@Carl Mummert: sorry, that was the comment reply userscript which was removing the spaces in the names. I fixed it. About proof-theory tag, I think a proof theorist (in the sense of Girard's "Proof Theory and Logical Complexity" or Troelstra and Schwichtenberg's "Basic Proof Theory") would probably disagree. Arithmetic would be a more suitable tag IMHO. –  Kaveh Jul 25 '11 at 1:23
@Kaveh: The 'arithmetic' tag is only for basic questions, though, according to its tag wiki. There are many topics that are lumped together in the proof theory MSC of 03F, and the 03F30 MSC code tends to be included on papers about this sort of topic. Thanks for fixing the user script, I realize I am unusually sensitive about that issue. –  Carl Mummert Jul 25 '11 at 1:38

Note that, in general, every axiom of $T$ is equivalent to the quantifier-free formula $0=0$ under the definition you have given. So for the first question it is sufficient to find any axiom that is not logically equivalent to a $\Sigma^0_1$ formula.

There is such an axiom for $Q$, namely $(\forall y)(y = 0 \lor (\exists x)(y = S(x)))$. This axiom is $\Pi^0_2$ and it cannot be logically equivalent to a $\Sigma^0_1$ formula because it is not preserved under taking superstructures.

The fact in my first paragraph also gives information on the second question, because it means that any arithmetical formula that is true in $\mathbb{N}$ is $\Sigma^0_1$ over $\operatorname{Th}(\mathbb{N})$. So all you need for the second question is a formula true in $\mathbb{N}$ but not equivalent to a $\Sigma^0_1$ formula over $Q$.

Furthermore, because $Q$ proves any true $\Sigma^0_1$ formula, it is sufficient to find any arithmetical formula that is true in $\mathbb{N}$ but not provable in $Q$. Because if a true formula $\phi$ was provably equivalent over $Q$ to a $\Sigma^0_1$ formula, then because the axioms of $Q$ are true the $\Sigma^0_1$ formula would be true, hence provable in $Q$, and thus $\phi$ would also be provable in $Q$. One concrete example of a true formula not provable in $Q$ is the Paris--Harrington principle.

-
+1, Your first paragraph gives a wonderful observation on the question! –  Asaf Karagila Jul 24 '11 at 22:34
Thanks!......... –  Carl Mummert Jul 24 '11 at 22:43
@CarlMummert: it does not need to be an axiom, formulas with lower logical complexity can prove new consequences of higher logical complexity. Nice point about the second question. :) –  Kaveh Jul 24 '11 at 23:47
Yes, of course. I only said that it is sufficient. I have edited my answer to include an explicit example I had pointed out in a comment. –  Carl Mummert Jul 25 '11 at 1:03
@Quinn: if you let $\psi(x)$ say "$x$ is not a coded proof of $0=1$ in $Q$" and you let $\phi(x)$ be the conjunction of that and the $\Pi^0_2$ axiom from my answer, that is an example of the kind you want, if I understand correctly. –  Carl Mummert Jul 26 '11 at 19:10

Yes, there are.

For the first question, let $\varphi(x) \in \Sigma_1$. Let $\varphi'(x)$ be $\varphi(x) \land \forall x\ (x=x)$.

For the second question, take an arbitrary formula $\varphi(x) \in \Sigma_1$. Let $T$ be a consistent recursively axiomatizable theory containt Robinson's $Q$. Let $\psi(x)$ be a formula that is true for all natural numbers (i.e. $\mathbb{N} \vDash \forall x \ \psi(x)$) but is not provable in $T$. Let $\varphi'(x)$ be $(\varphi(x) \land \psi(x)) \lor (\lnot \varphi(x) \land \lnot \psi(x))$. It is clear that $\mathbb{N} \vDash \forall x \ (\varphi(x) \leftrightarrow \varphi'(x)$. On the other hand $T \nvdash \forall x \ (\varphi(x) \leftrightarrow \varphi'(x))$ since that would imply $T \vdash \forall x \ \psi(x)$. Edit: This only shows that $\varphi'$ is not equivalent to the original formula, not that it is not provable $\Sigma_1$.

I think the answer is still yes since a no answer would imply that the set of $T$-provably $\Sigma_1$ formulas are effectively enumerable which I think is false. But I don't have a short poof for it or a reference. I will update the answer when I find it. (still I think there should be an easier proof).

-
Mightn't $\varphi'(x)$ still be $\Sigma_{1}$ in $T$? That is, mightn't $T \vdash \forall x (\varphi' \leftrightarrow \pi)$ for some formula $\pi$ (which must be different from $\varphi$ by your argument)? For example, if $\psi(x)$ says "$x$ is not the code of a proof of $0=1$", then $\psi \in \Delta_{0}$. So won't $\varphi'(x)$ be $\Sigma_{1}$ over $\emptyset$? –  Quinn Culver Jul 24 '11 at 19:29
For the first question, I would say a formula in $\Sigma^0_1$ if it is logically equivalent to a formula with only existential quantifiers (that is, provably equivalent without using any non-logical axioms, but allowing the use of the usual logical axioms and rules of inference). So the first example you give is not an example under my definitions. However, the Wikipedia article for Robinson arithmetic shows it has a $\Pi^0_2$ axiom $(\forall y) ( y = 0 \lor (\exists x) (y = S(x)))$. If you replace $(\forall x)(x = x)$ in the first example with this, I think it may work (still needs proof). –  Carl Mummert Jul 24 '11 at 22:15
@CarlMummert: I think that is not how it is defined usually. I think that would be called provably $\Sigma_1$. That would make the class of $\Sigma_1$ formulas dependent on the theory which is not the usual practice AFAIK. –  Kaveh Jul 24 '11 at 23:45
@Kaveh: both conventions are certainly used, but in my work in the area I would use the stronger one. Otherwise one has the inelegant result that not every arithmetical formula is classified in the arithmetical hierarchy, they are only equivalent to formulas in the hierarchy. Moreover, as your answer shows, the weaker definition trivializes the first part of the question by allowing you to adjoin a logical validity to a formula. But it is possible to give a non-trivial answer that also works with the stronger version. –  Carl Mummert Jul 25 '11 at 0:59
@CarlMummert: you are right, good point. –  Kaveh Jul 25 '11 at 1:01