Skip to main content
added 303 characters in body
Source Link
Henry Towsner
  • 7.1k
  • 27
  • 35

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.

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

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.

Source Link
Henry Towsner
  • 7.1k
  • 27
  • 35

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