Hierarchical formula classes with respect to semi-classical prenex normalization

TL;DR

This paper introduces new classes of first-order formulas, refining existing classes, to better understand semi-classical prenex normalization and its limitations in constructive theories.

Contribution

It defines the classes E_k^n and U_k^n, showing they precisely correspond to  ext{Sigma}_k and  ext{Pi}_k classes under n-th level semi-classical prenex normalization, refining previous classes.

Findings

Introduced classes E_k^n and U_k^n for semi-classical prenex normalization.

Established the correspondence of these classes with  ext{Sigma}_k and  ext{Pi}_k.

Connected the classes to intuitionistic arithmetic with restricted law-of-excluded-middle.

Abstract

In [10], the authors formalized the standard transformation procedure for prenex normalization of first-order formulas and showed that the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ introduced in Akama et al. [1] are exactly the classes induced by $\Sigma_k$ and $\Pi_k$ respectively via the transformation procedure. In that sense, the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ correspond to $\Sigma_k$ and $\Pi_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 $\mathcal{E}_k^n$ and $\mathcal{U}_k^n$ of first-order 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, 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 $\Sigma_n$-form. In fact, if $ n\geq k$, our classes $\mathcal{E}_k^n$ and $\mathcal{U}_k^n$ are identical with the cumulative variants $\mathrm{E}^+_k$ and $\mathrm{U}^+_k$ of $\mathrm{E}_k$ and $\mathrm{U}_k$ respectively. In this sense, our classes are refinements of $\mathrm{E}^+_k$ and $\mathrm{U}^+_k$ with respect to the prenex normalization from the semi-classical perspective.