Conservation theorems on semi-classical arithmetic

TL;DR

This paper explores the relationships between classical and semi-classical arithmetic theories, establishing optimal conservation theorems and characterizing the structure of classical principles within the arithmetical hierarchy.

Contribution

It provides a new structured proof of conservation theorems using a generalized negative translation and characterizes the optimality of these theorems for semi-classical arithmetic.

Findings

PA is $ ext{Pi}_{k+2}$-conservative over $ ext{HA} + ext{Sigma}_k ext{-LEM}$

Conservation theorems are optimal and characterize the provability of $ ext{Sigma}_k ext{-LEM}$

The structure of conservation theorems aligns with the arithmetical hierarchy of classical principles.

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.