# Formula that requires a higher complexity to be proved

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?

• @EmilJeřábek That should be an answer! Jan 19, 2021 at 19:21
• @EmilJeřábek if you provide your two comments as an answer (maybe expanding a little - as I said, my knowledge of this topics is rather primitive), I'd be glad to accept it! Jan 20, 2021 at 10:37
• That's interesting if the ∀ϵ∃δ formulas are a real source of the well-known stumbling blocks for calculus students. I wonder if it would help to explain the logical structure of the definition and give other examples of similar structure, like the Twin Primes conjecture (another ∀ϵ∃δ statement), before getting to similar formulas in calculus. It might also be fun to describe the statement of Waring's problem,which is ∀k∃s∀n.
– none
Jan 28, 2021 at 20:31

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