# Prenex normalization and the hierarchical classification of formulas

## TL;DR

This paper justifies a hierarchical classification of first-order formulas within a general first-order theory context, linking it to prenex normalization procedures and standard classes like  and .

## Contribution

It formalizes the prenex normalization process and shows the classes _k and _k correspond to _k and _k classes under this process in any first-order theory.

## Key findings

- Classes _k and _k are exactly the classes induced by _k and _k via prenex normalization.
- The hierarchical classification applies broadly in first-order theories.
- The paper provides a formal justification for the classification scheme.

## Abstract

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 $\Sigma_k$ and $\Pi_k$ respectively via the transformation procedure in any first-order theory.