Conservation theorems on semi-classical arithmetic

Abstract

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 new 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.

32 pages