3
$\begingroup$

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.

  • 0
    @Carl Mummert: you are right [MSC](http://www.ams.org/mathscinet/msc/msc2010.html?t=03Fxx&btn=Current) that it is in MSC 3F, but 3F is not proof theory, it is also constructive mathematics (which is probably why fragments of arithmetic are place there). AFAIU proof theory means dealing with proofs themselves whereas nothing in this question is about proofs as the main objects of interest, at least that is what people I would call proof theorists write. Maybe we should create a a new tag for fragments-of-arithmetic or arithmetic-theory? I will check to see what is being used for the topic on MO2011-07-25

2 Answers 2

3

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
    @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.2011-07-26
0

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).

  • 0
    @CarlMummert: you are right, good point.2011-07-25