Prenex normalization and the hierarchical classification of formulas

2023/02/23 by M. Fujiwara, Fujiwara, Makoto, Taishi Kurahashi +1 · 1 citation
Computer Science · #FOS: Mathematics #Logic (math.LO) #Logic, programming, and type systems #Numerical Methods and Algorithms #Polynomial and algebraic computation

paper · pdf · doi:10.48550/arxiv.2302.11808

openalex publication_date 2023/02/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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 E_k and U_k introduced in [1] are exactly the classes induced by Σ_k and Π_k respectively via the transformation procedure in any first-order theory.

Cited by

• Hierarchical formula classes with respect to semi-classical prenex normalization

Related

• Hierarchical formula classes with respect to semi-classical prenex normalization
• A unified approach to the theory of normed structures - Part I: The single-sorted case
• Refining the arithmetical hierarchy of classical principles
• Formulas and properties
• On first-order arithmetic truth