Conservation Theorems on Semi-Classical Arithmetic

Journal of Symbolic Logic 88 (4):1469-1496 (2023)
  Copy   BIBTEX


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.



    Upload a copy of this work     Papers currently archived: 92,907

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Whither relevant arithmetic?Harvey Friedman & Robert K. Meyer - 1992 - Journal of Symbolic Logic 57 (3):824-831.
Some preservation theorems in an intermediate logic.Seyed M. Bagheri - 2006 - Mathematical Logic Quarterly 52 (2):125-133.
Borel quasi-orderings in subsystems of second-order arithmetic.Alberto Marcone - 1991 - Annals of Pure and Applied Logic 54 (3):265-291.
Classical arithmetic as part of intuitionistic arithmetic.Michael Potter - 1998 - Grazer Philosophische Studien 55 (1):127-41.
The Gödel Incompleteness Theorems (1931) by the Axiom of Choice.Vasil Penchev - 2020 - Econometrics: Mathematical Methods and Programming eJournal (Elsevier: SSRN) 13 (39):1-4.
Illusory models of peano arithmetic.Makoto Kikuchi & Taishi Kurahashi - 2016 - Journal of Symbolic Logic 81 (3):1163-1175.
Formalizing forcing arguments in subsystems of second-order arithmetic.Jeremy Avigad - 1996 - Annals of Pure and Applied Logic 82 (2):165-191.


Added to PP

16 (#930,647)

6 months
13 (#218,677)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Constructivism in Mathematics, An Introduction.A. Troelstra & D. Van Dalen - 1991 - Tijdschrift Voor Filosofie 53 (3):569-570.
Some Conservative Extension Results on Classical and Intuitionistic Sequent Calculi.Hajime Ishihara - 2012 - In Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation. De Gruyter. pp. 289-304.

Add more references