Epsilon substitution for ID₁ via cut-elimination

DOI10.1007/S00153-017-0590-3MaRDI QIDQ1661673zbMATH OpenOpenAlexFDO

Authors Henry Towsner

Publication date 16 August 2018

Published in Archive for Mathematical Logic (Search for Journal in Brave)

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

zbMATH Keywords

epsilon substitutiontermination proofordinal interpretation

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35)

Abstract: The $epsilon$-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory $I{D}_1$ using a variant of the cut-elimination formalism introduced by Mints.

Recommendations

• Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
• A method of epsilon substitution for the predicate logic with equality
• scientific article; zbMATH DE number 6307937
• Cut elimination for a simple formulation of epsilon calculus
• A termination proof for epsilon substitution using partial derivations

Cites work

• scientific article; zbMATH DE number 4039890 (Why is no real title available?)
• scientific article; zbMATH DE number 733386 (Why is no real title available?)
• scientific article; zbMATH DE number 1418438 (Why is no real title available?)
• scientific article; zbMATH DE number 6307937 (Why is no real title available?)
• scientific article; zbMATH DE number 3334141 (Why is no real title available?)
• scientific article; zbMATH DE number 3061667 (Why is no real title available?)
• A system of abstract constructive ordinals
• An ordinal analysis of parameter free \(\Pi^{1}_{2}\)-comprehension
• An ordinal analysis of stability
• Consistency proofs of subsystems of classical analysis
• Cut-elimination for impredicative infinitary systems part I. Ordinal-analysis for ID1
• Epsilon substitution for transfinite induction
• Epsilon substitution method for -FIX
• Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
• Epsilon substitution method for elementary analysis
• Epsilon substitution method for theories of jump hierarchies
• Investigations of subsystems of second order arithmetic and set theory in strength between \(\Pi^1_1\)-CA and \(\Delta^1_2\)-\(\text{CA}+\text{BI}\). I
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Non-deterministic Epsilon Substitution Method for PA and ID 1
• Proof theory for theories of ordinals. I: Recursively Mahlo ordinals
• Proof theory for theories of ordinals. II: \(\Pi_{3}\)-reflection
• Proof theory. The first step into impredicativity
• Proof-theoretic analysis of KPM
• Recent Advances in Ordinal Analysis: Π¹₂— CA and Related Systems
• Subsystems of second order arithmetic
• The consistency of arithmetics
• Zur Widerspruchsfreiheit der Zahlentheorie

Cited in

(4)

• Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
• Explaining the Gentzen-Takeuti reduction steps: A second-order system
• Cut-elimination for \(\omega_{1}\)
• scientific article; zbMATH DE number 6307937 (Why is no real title available?)

This page was built for publication: Epsilon substitution for \(ID_1\) via cut-elimination

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