CONSERVATION THEOREMS ON SEMI-CLASSICAL ARITHMETIC

DOI10.1017/JSL.2022.25MaRDI QIDQ6180604zbMATH OpenOpenAlexWikidataFDO

Authors Makoto Fujiwara, Taishi Kurahashi

Publication date 22 December 2023

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2107.11356

zbMATH Keywords

intuitionistic arithmeticconservation theoremssemi-classical arithmetic

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50)

Abstract: We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $mathsfPA$ and intuitionistic arithmetic $mathsfHA$. Using a generalized negative translation, we first provide a new structured proof of the fact that $mathsfPA$ is $P{i}_{k+2}$-conservative over $mathsfHA+Sigm{a}_{k}ext-mathrmLEM$ where $Sigm{a}_{k}ext-mathrmLEM$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $Sigm{a}_k$. In addition, we show that this conservation theorem is optimal in the sense that for any semi-classical arithmetic $T$, if $mathsfPA$ is $P{i}_{k+2}$-conservative over $T$, then $T$ proves $Sigm{a}_{k}ext-mathrmLEM$. 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.

Cites work

• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• scientific article; zbMATH DE number 1170091 (Why is no real title available?)
• scientific article; zbMATH DE number 1406469 (Why is no real title available?)
• Constructivism in mathematics. An introduction. Volume II
• EXTENDED FRAMES AND SEPARATIONS OF LOGICAL PRINCIPLES
• Fluctuations, effective learnability and metastability in analysis
• Logic and structure
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On parameter free induction schemas
• Prenex normal form theorems in semi-classical arithmetic
• Refining the arithmetical hierarchy of classical principles
• Some conservative extension results on classical and intuitionistic sequent calculi

Cited in

(1)

• A generalization of a conservativity theorem for classical versus intuitionistic arithmetic

This page was built for publication: CONSERVATION THEOREMS ON SEMI-CLASSICAL ARITHMETIC

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6180604)