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



What are key $\Sigma^0_2$ or $\Pi^0_3$ theorems?
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.


