Harrington's conservation theorem redone
From MaRDI portal
Publication:948908
DOI10.1007/s00153-008-0080-8zbMath1160.03039MaRDI QIDQ948908
Gilda Ferreira, Fernando Ferreira
Publication date: 16 October 2008
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00153-008-0080-8
cut-elimination; second-order arithmetic; bounded formula; system \(\text{WKL}_0\), \(\text{RCA}_0\) \(\Pi^1_1\)-conservativity; Weak König's Lemma
03F05: Cut-elimination and normal-form theorems
03F07: Structure of proofs
03F35: Second- and higher-order arithmetic and fragments
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A simple proof of Parsons' theorem
- Fragments of arithmetic
- Remarks on Herbrand normal forms and Herbrand realizations
- Bounded functional interpretation
- Formalizing forcing arguments in subsystems of second-order arithmetic
- Herbrand analyses
- Strict \({\varPi^1_1}\)-reflection in bounded arithmetic
- Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
- A feasible theory for analysis