Formula that requires a higher complexity to be proved

Question

Sorry if this question is naive, I am not very well versed in recursion theory.

Does it exist a formula $\phi$ such that:

• $\phi$ is provable in Peano arithmetic
• $\phi \in \Sigma^0_n$ or $\phi \in \Pi^0_n$, but
• provably, every proof of $\phi$ from the axioms must involve a step that does not belong to $\Sigma^0_k$ or $\Pi^0_k$ for any $k \leq n$? Or even a step that needs complexity at least $\Sigma^0_{n + m}$ or $\Pi_{n + m}$ for some $m > 1$?

This may even not be well defined - it could depend on the proof system - but even a result for a particular proof system could be interesting.

What I am trying to capture is the following. Young mathematicians often struggle with calculus, since for the first time they have to deal with formulas involving two quantifieres ($\forall \epsilon \exists \delta \dots$). Of course, with experience, they come to manage these formulas without trouble.

But juggling many more quantifiers quickly becomes overwhelming even for expert mathematicians. Could it be the case that there exists some claim of interest to mathematicians (involving few quantifiers) but such that in order to prove it we need to consider intermediate steps that are too complex for our feeble minds?

Answer 1

First, let me mention that the only way a formula may require proofs using complex formulas is that it requires complex axioms to prove: the cut elimination theorem implies that if a $\Sigma_n$ formula is provable from $\Sigma_n$ axioms, it has a proof from these axioms in which all formulas are $\Sigma_n$; and similarly for $\Pi_n$ in place of $\Sigma_n$. (Literally, this holds for the sequent calculus. When we use a different proof system, such as some form of a Hilbert calculus, we may need to raise the complexity by a small constant.)

In particular, up to small constants, no such formulas exist when Peano arithmetic is replaced in the question by a finitely axiomatizable theory such as $I\Sigma_n$ (= Peano arithmetic with the induction schema restricted to $\Sigma_n$ formulas).

However, such formulas do exist for Peano arithmetic, and we might even take $\phi\in\Pi_1$ irrespective of $n$: for example, let $\phi=\mathrm{Con}_{I\Sigma_n}$ (the formalized consistency statement for $I\Sigma_n$). It is known that $\mathrm{PA}\vdash\mathrm{Con}_{I\Sigma_n}$ (see also here for a more general result), but Gödel’s second incompleteness theorem shows that $I\Sigma_n\nvdash\mathrm{Con}_{I\Sigma_n}$; thus, any proof of $\mathrm{Con}_{I\Sigma_n}$ in $\mathrm{PA}$ must use an instance of the induction schema for formulas of higher complexity than $\Sigma_n$ (and higher than $\Pi_n$, as $I\Sigma_n=I\Pi_n$).