2025/06/27 by Makoto Fujiwara, Fujiwara, Makoto, Taishi Kurahashi +1
Computer Science · #Logic, programming, and type systems #semigroups and automata theory #Advanced Algebra and Logic
paper · pdf · doi:10.48550/arxiv.2506.22348
In [10], the authors formalized the standard transformation procedure for prenex normalization of first-order formulas and showed that the classes Ek and Uk introduced in Akama et al. [1] are exactly the classes induced by Σk and Πk respectively via the transformation procedure. In that sense, the classes Ek and Uk correspond to Σk and Πk based on classical logic respectively. On the other hand, some transformations of the prenex normalization are not possible in constructive theories. In this paper, we introduce new classes Ekn and Ukn of first-order formulas with two parameters k and n, and show that they are exactly the classes induced by Σk and Πk respectively according to the n-th level semi-classical prenex normalization, which is obtained by the prenex normalization in [10] with some restriction to the introduced classes of degree n. In particular, the latter corresponds to possible transformations in intuitionistic arithmetic augmented with the law-of-excluded-middle schema restricted to formulas of Σn-form. In fact, if n≥ k, our classes Ekn and Ukn are identical with the cumulative variants E+k and U+k of Ek and Uk respectively. In this sense, our classes are refinements of E+k and U+k with respect to the prenex normalization from the semi-classical perspective.