Prenex normalization and the hierarchical classification of formulas

Akama et al. [1] introduced a hierarchical classification of first-order formulas for a hierarchical prenex normal form theorem in semi-classical arithmetic. In this paper, we give a justification for the hierarchical classification in a general context of first-order theories. To this end, we first formalize the standard transformation procedure for prenex normalization. Then we show that the classes ${\mathrm{E}}_k$ and ${\mathrm{U}}_k$ introduced in [1] are exactly the classes induced by ${\mathrm{\Sigma }}_k$ and ${\mathrm{\Pi }}_k$ respectively via the transformation procedure in any first-order theory.