arXiv · 2302.11808
Prenex normalization and the hierarchical classification of formulas
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.
Explore related subjects
Keep this discovery
Makoto Fujiwara, Taishi Kurahashi. 2023-02-23. Prenex normalization and the hierarchical classification of formulas. https://arxiv.org/abs/2302.11808
Cite the original work for its findings. Save a collection to share your selection of sources.