Hierarchical formula classes with respect to semi-classical prenex normalization
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913915519107072 |
|---|---|
| author | Fujiwara, Makoto Kurahashi, Taishi |
| author_facet | Fujiwara, Makoto Kurahashi, Taishi |
| contents | 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 $Σ_k$ and $Π_k$ respectively via the transformation procedure. In that sense, the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ 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 $\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 $Σ_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\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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_22348 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Hierarchical formula classes with respect to semi-classical prenex normalization Fujiwara, Makoto Kurahashi, Taishi Logic 03B20, 03F03, 03F50 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 $Σ_k$ and $Π_k$ respectively via the transformation procedure. In that sense, the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ 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 $\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 $Σ_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\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. |
| title | Hierarchical formula classes with respect to semi-classical prenex normalization |
| topic | Logic 03B20, 03F03, 03F50 |
| url | https://arxiv.org/abs/2506.22348 |