5
$\begingroup$

I am researching a logical system that is limited to $\Pi^0_2$ sentences and I am busy to prove that FOL + PA is a conservative extension of that system. Meaning that with $\Sigma^0_n$ sentences (that are not $\Pi^0_2$) you can express things, but they are not really necessary for proving a $\Pi^0_2$ theorem.

As part of this research I like to know if there are interesting/notable theorems in literature that actually proves a $\Sigma^0_n$ or $\Pi^0_{n+1}$ with $n \geq 2$ sentence (which is not $\Pi^0_2$). Such example would contradict my idea, because if according to my idea those sentences are not necessary, they are likely not be interesting. So, if they exists I like to study it.

Note, that if you use the axiom scheme for induction (in a notable proof) you may temporarily have a $\Pi^0_3$ sentence, but the obtained implication is mostly directly used and than falls back to a $\Pi^0_2$ sentence. So, I am not looking for that.

Finally, the result is different than with allowing to quantify over predicates, which does add strength and can prove things about ordinals etc.

Thanks in advance

Improve this question
$\endgroup$
7
  • 4
    $\begingroup$ I don't completely understand the first paragraph. $\text{Con}(\text{PA})$ is a $\Sigma^0_2$ sentence that does add strength to PA. At the same time, many theorems in the literature are $\Pi^1_1$ or $\Pi^1_2$, rather than arithmetical. If no set parameters are allowed, then it is hard to state most ordinary theorems. $\endgroup$
    – Carl Mummert
    Aug 23, 2015 at 0:11
  • 2
    $\begingroup$ Although I'm not a number theorist and therefore can't immediately give you details, I believe that there are some important results saying that certain Diophantine equations have only finitely many solutions, without giving an explicit bound for those solutions. The natural formalization of such a statement would be a $\Sigma^0_2$ sentence. $\endgroup$
    – Andreas Blass
    Aug 23, 2015 at 8:36
  • 2
    $\begingroup$ PA proves the consistency of the $\Sigma^0_n$ fragment of PA, and this is a $\Pi^0_1$ assertion, and hence $\Sigma^0_2$. Does your system prove the consistency of all these fragments of PA? This would be required for your conservativity result. $\endgroup$
    – Joel David Hamkins
    Aug 23, 2015 at 9:54
  • 2
    $\begingroup$ Even better, the $\Pi^0_2$ fragment of PA is axiomatized by the uniform $\Sigma_1$ reflection schema for finite subtheries of PA (that is, for the theories $I\Sigma_n$) $\endgroup$
    – Emil Jeřábek
    Aug 23, 2015 at 10:17
  • 1
    $\begingroup$ @JoelDavidHamkins and Emil Thanks for the replies, but I have difficulty to follow this, but I will see what I can find in my books and on the internet. But the last few weeks I had quite a progress in my proof. For any $\Pi^0_2$ theorem that has a proof that contains sentences not $\Pi^0_2$ I have several rewriting steps. One with Herbrandization, where I later replace the Herbrand functions. This does not work for induction, but I think I found a solution for that. But of course, until I completely worked it out, it can have a terrible flaw. $\endgroup$
    – Lucas K.
    Aug 23, 2015 at 11:25

1 Answer 1

Reset to default
7
$\begingroup$

I'm not clear whether you're asking if there are any interesting non-$\Pi_2$ theorems in the literature, or any proofs of $\Pi_2$ theorems with interesting non-$\Pi_2$ intermediate steps which cannot be removed.

If your question is whether there are interesting $\Sigma_2$ or higher theorems in the mathematical literature, the answer is a great many of them. Off the top of my head, the Thue-Sigel-Roth and Skolem–Mahler–Lech theorems are good examples. (I believe these are both $\Pi_3$.)

If your question is whether those theorems are necessary to prove $\Pi_2$ consequences, the answer is no. In general, if $PA$ proves a $\Pi_2$ statement then there is a constructive proof consisting only of $\Pi_2$ statements. The usual proof of this works in $PA^\omega$ ($PA$ with constructive higher types) so that high quantifier complexity statements can be replaced by statements with functionals using the functional interpretation, and so the $\Pi_2$ statements in question involve quantifiers over computable functionals. If you prefer to stick to $PA$, all these quantifiers over computable functionals can be replaced by quantifiers over numbers viewed as indices for Turing machines computing the functional. (The coding gets messy, since one can't computably tell whether one has a computable functional, but this can be resolved while staying in a $\Pi_2$ format.)

EDITED: I should clarify that last bit. If one stays in PA, one gets a proof of $\exists y\phi(n,y)$ for each $n$ in a uniform(-ish) way using only $\Pi_2$ statements; if you actually want a purely $\Pi_2$ proof of the whole $\Pi_2$ statement, one does have to work in a somewhat expanded language.

Improve this answer
$\endgroup$
8
  • $\begingroup$ Many thanks. I will study is, can't judge it immediately. I think this is a very notable result, for several reasons. In reverse mathematics PA and $ACA_0$ are in the same class. Now this range is extended to a system that is less expressive. Also, since $\Pi_2$ has far stronger relation with computation than PA in general, this makes logic and computability theory stronger linked. $\endgroup$
    – Lucas K.
    Aug 23, 2015 at 21:52
  • $\begingroup$ With this result I can show that PA (and $ACA_0$) is a conservative extension of Primitive Closure Arithmetic, which I designed, see mathoverflow.net/questions/208696/primitive-closure-arithmetic. This is a very simple system closely related to computation $\endgroup$
    – Lucas K.
    Aug 23, 2015 at 21:54
  • $\begingroup$ I have looked in your notes on your homepage and as far I understand, the proof doesn't require transfinite induction. $\endgroup$
    – Lucas K.
    Aug 23, 2015 at 21:58
  • $\begingroup$ @LucasK.: The description of PCA in mathoverflow.net/q/208696 does not seem to include anything that would not formalize in $I\Sigma_1$, or for that matter in its $\Pi_2$ fragment, which is just PRA. Thus, PCA should be equivalent (or at least, included in) PRA, and much weaker than the $\Pi_2$ fragment of PA. $\endgroup$
    – Emil Jeřábek
    Aug 24, 2015 at 14:19
  • $\begingroup$ @EmilJeřábek No that is not true. PCA has closures. The difference between a recursive function and a closure is that a closure isn't guaranteed to terminate. This is comparable to adding an unbound existential quantifier. Where PRA is $\Pi_1$ PCA is $\Pi_2$, due to the existential quantifier. This unbound existential quantifier is also allowed in the induction step, making it stronger than PRA. I was not sure whether PCA was something between PRA and PA or equal strength of PA. Given the answer of Henry, I am more convinced of the latter, but every detail has to be worked out. $\endgroup$
    – Lucas K.
    Aug 24, 2015 at 15:00

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.