Conservation Theorems on Semi-Classical Arithmetic

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

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

Links

PhilArchive



    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.

Analytics

Added to PP
2022-04-08

Downloads
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