We refine the arithmetical hierarchy of various classical principles by finely investigating the derivability relations between these principles over Heyting arithmetic. We mainly investigate some restricted versions of the law of excluded middle, De Morgan's law, the double negation elimination, the collection principle and the constant domain axiom.

Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate way which still serves (...) to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is $\Pi _2$ -conservative over intuitionistic arithmetic. (shrink)

We systematically study the interrelations between all possible variations of Δ10\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Delta ^0_1$$\end{document} variants of the law of excluded middle and related principles in the context of intuitionistic arithmetic and analysis.

We systematically study the interrelations between all possible variations of \(\Delta ^0_1\) variants of the law of excluded middle and related principles in the context of intuitionistic arithmetic and analysis.

We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf {PA}$ and intuitionistic arithmetic $\mathsf {HA}$. Using a generalized negative translation, we first provide a structured proof of the fact that $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over $\mathsf {HA} + {\Sigma _k}\text {-}\mathrm {LEM}$ where ${\Sigma _k}\text {-}\mathrm {LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $\Sigma _k$. In addition, we show that this conservation theorem is optimal in the (...) sense that for any semi-classical arithmetic T, if $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over T, then ${T}$ proves ${\Sigma _k}\text {-}\mathrm {LEM}$. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles. (shrink)