Akama et al. [1] introduced a hierarchical classification of first-order formulas and investigated them in the context of semi-classical arithmetic. In this talk, we first give a justification for the hierarchical classification in a general context of first-order theories. In fact, we formalize the standard transformation procedure for prenex normalization, and show that the classes E_k and U_k introduced in [1] are exactly the classes induced by Sigma_k and Pi_k respectively via the transformation procedure. See [2] for the details. In addition, we restrict the prenex normalization procedures to those which are possible over intuitionistic logic with assuming the decidability of formulas of degree n. Then we introduce new classes E^n_k and U^n_k of formulas with two parameters k and n, and show that they are exactly the classes induced by Sigma_k and Pi_k respectively according to the n-th level semi-classical prenex normalization. This is a joint work with Taishi Kurahashi.

[1] Yohji Akama, Stefano Berardi, Susumu Hayashi, and Ulrich Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS ’04), pp.192–201, 2004.

[2] Makoto Fujiwara and Taishi Kurahashi, Prenex normalization and the hierarchical classification of formulas, Archive for Mathematical Logic, vol. 63, pp. 391-403, 2024.