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?