CONSERVATION THEOREMS ON SEMI-CLASSICAL ARITHMETIC

DOI10.1017/JSL.2022.25arXiv2107.11356OpenAlexW3184417074WikidataQ113858279 ScholiaQ113858279MaRDI QIDQ6180604FDOQ6180604

Taishi Kurahashi, Makoto Fujiwara

Publication date: 22 December 2023

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

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.

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logic and structure
• Constructivism in mathematics. An introduction. Volume II
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Fluctuations, effective learnability and metastability in analysis
• On parameter free induction schemas
• PRENEX NORMAL FORM THEOREMS IN SEMI-CLASSICAL ARITHMETIC
• Refining the arithmetical hierarchy of classical principles
• EXTENDED FRAMES AND SEPARATIONS OF LOGICAL PRINCIPLES

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)