# Does this sketch proof that every formula is equivalent to one in the arithmetical hierarchy work?

In the lecture notes for my course, the arithmetical hierarchy is defined as follows:

• A formula is $\Sigma_0$ or $\Pi_0$ if every quantifier is bound;
• A formula is $\Sigma_{n+1}$ if it is of the form $\exists x F(x)$ where $F(x)$ is $\Pi_n$;
• A formula is $\Pi_{n+1}$ if it is of the form $\forall x F(x)$ where $F(x)$ is $\Sigma_n$.

We then prove that every formula is equivalent to a $\Sigma_n$ or $\Pi_n$ formula, for some $n$. The proof runs essentially like this: given a formula $F$, find a prenex normal form for it, and then "collapse" the adjacent quantifiers of the same type, using a bijection between $\mathbb{N}^2$ and $\mathbb{N}$.

My question is as follows: could we, instead of collapsing adjacent quantifiers, simply add "interpolating" quantifiers that do nothing instead? So for example, if $\exists x \exists y$ occurs in the prenex normal form of our formula, we find some fresh variable $z$ and put a universal quantification in between the two existential ones, to get $\exists x \forall z \exists y$.

Of course, this won't be as efficient as the other proof in that we won't get as low a class in the arithmetical hierarchy, but it seems to me that if all we want to do is prove every formula is equivalent to one in the arithmetical hierarchy, this way involves much less mess.

(Please do let me know if there's anything wrong with this question - it's my first one! Thanks for your patience.)

The collapsing concept is of independent interest, however, for judging by eye how far down in the hierarchy a given formula can be pushed. So one will want to develop that anyway. Otherwise you're going to be confused when people say that such-and-such is obviously, say, a $\Sigma_2^0$ formula.
• @AlexMcKenzie: Not sure what "PNF" means here, but there cannot be such an algorithm, since it is undecidable whether a given formula is always true (which would make it $\Delta_0$). Even if we're only looking for formulas that are provably always true, that too is undecidable. – Henning Makholm Apr 12 '16 at 14:02