Harrington's conservation theorem redone
type: Item
instance of: scholarly article
title: Harrington's conservation theorem redone
zbMATH Open document ID: 1160.03039
author: Fernando Ferreira
author: Gilda Ferreira
published in: Archive for Mathematical Logic
publication date: 2008-10-16T00:00:00Z
review text: The theorem in the title states that the second-order arithmetic \(\text{WKL}_0\) is \(\Pi^1_1\)-conservative over the theory \(\text{RCA}_0\). Harrington proved this model-theoretically, previously. Now, the authors give a proof-theoretic proof. Their set-up is sequent calculus, and they replace Weak König's Lemma (in \(\text{WKL}_0)\) by its contrapositive, \(\text{FAN}_0\), formulated as a rule. Given a (formal) poof of a \(\Pi^1_1\)-formula \(XF(X)\), they use the method of cut elimination so that in the resulting proof of \(F(X)\) only \(\Sigma^0_1\)-formulas occur (certainly no second-order quantifier). The authors' crucial observation is that a bounded formula can be regulated, and so this new proof is normalized further. This step requires case analysis of each rule, but shows that the \(\text{FAN}_0\)-rule is not necessary. In the last section, the authors make observations on contrast between classical and intuitionistic systems. For instance, the conservation theorem of the above type does not hold intuitionistically. On the other hand, the theory \(\text{RCA}_0^-+\text{FAN}\) is inconsistent classically, but intuitionistically it is \(\Pi^0_2\)-conservative over PRA.
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F07
zbMATH DE Number: 5351800
zbMATH Keywords: system \(\text{WKL}_0\), \(\text{RCA}_0\) \(\Pi^1_1\)-conservativity
zbMATH Keywords: bounded formula
zbMATH Keywords: second-order arithmetic
zbMATH Keywords: Weak König's Lemma
zbMATH Keywords: cut-elimination
MaRDI profile type: Publication
full work available at URL: s00153-008-0080-8
OpenAlex ID: W1985240925
cites work: Formalizing forcing arguments in subsystems of second-order arithmetic
cites work: Q4215634
cites work: Q4215631
cites work: Q4215630
cites work: Strict \({\varPi^1_1}\)-reflection in bounded arithmetic
cites work: A feasible theory for analysis
cites work: A simple proof of Parsons' theorem
cites work: Bounded functional interpretation
cites work: Q4001935
cites work: Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
cites work: Remarks on Herbrand normal forms and Herbrand realizations
cites work: Q5600870
cites work: Fragments of arithmetic
cites work: Herbrand analyses
cites work: Q4220572
cites work: Q4729781
DOI: 10.1007/S00153-008-0080-8
Recommended article: Q4281472
Recommended article: A new conservation theorem
Recommended article: Hodge decomposition and conservation laws
Recommended article: Q3825001
Recommended article: Q5687456
Recommended article: Redheffer's theorem revisited
Recommended article: A new technique for preserving conservation laws
Recommended article: Conservation laws and null divergences
Recommended article: Q4852713
Recommended article: The absolute invariance of conservation laws
description: scientific article; zbMATH DE number 5351800