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
    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.2011-07-24
  • 0
    @CarlMummert: I don't think this is a proof-theory question.2011-07-24
  • 0
    @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.2011-07-25
  • 0
    @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.2011-07-25
  • 0
    @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.2011-07-25
  • 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
    +1, Your first paragraph gives a wonderful observation on the question!2011-07-24
  • 0
    @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. :)2011-07-24
  • 1
    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.2011-07-25
  • 0
    @Carl Your answer is great, but this isn't really what I had in mind. I wanted a non-sentence formula $\varphi$ such that $Th(\mathbb{N})$ proves is (equivalent to a) $\Sigma_{1}$ but $Q$ doesn't. Should I ask this as a new question or edit this one?2011-07-26
  • 0
    @Quinn: I don't quite follow what you're looking for. $\operatorname{Th}(\mathbb{N})$ proves the Paris-Harrington principle is equivalent to $0=0$ but $Q$ doesn't prove it's equivalent to any $\Sigma^0_1$ formula. If you want to make it not a sentence, you can follow Kaveh's method and add "$\land (n = n)$ " to the end.2011-07-26
  • 0
    @Carl For a complete theory, what I'm asking might not make sense. What I'm trying to capture is that the theory $T$ doesn't know much about the truth of $\varphi$, yet knows that $\varphi$ is equivalent to a $\Sigma_{1}$ formula. So what about a formula $\varphi(x)$ with one free variable such that $Q \nvdash \forall x \varphi(x)$, $Q \nvdash \forall x \neg \varphi(x)$ and $Q \vdash \varphi(x) \leftrightarrow \psi$ for some $\psi \in \Sigma_{1}$, but $\emptyset \nvdash \varphi(x) \leftrightarrow \psi$?2011-07-26
  • 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
    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$?2011-07-24
  • 0
    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).2011-07-24
  • 0
    @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.2011-07-24
  • 0
    @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.2011-07-25
  • 0
    @CarlMummert: you are right, good point.2011-07-25