Epsilon substitution for ID₁ via cut-elimination

DOI10.1007/S00153-017-0590-3zbMATH Open1455.03075arXiv1509.00390OpenAlexW2756418407MaRDI QIDQ1661673FDOQ1661673

Henry Towsner

Publication date: 16 August 2018

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

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.

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

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

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)

Cites Work

• Epsilon substitution method for elementary analysis
• Title not available (Why is that?)
• The consistency of arithmetics
• Consistency proofs of subsystems of classical analysis
• A system of abstract constructive ordinals
• Proof theory. The first step into impredicativity
• Title not available (Why is that?)
• Proof theory for theories of ordinals. I: Recursively Mahlo ordinals
• An ordinal analysis of stability
• An ordinal analysis of parameter free \(\Pi^{1}_{2}\)-comprehension
• Proof theory for theories of ordinals. II: \(\Pi_{3}\)-reflection
• Recent Advances in Ordinal Analysis: Π¹₂— CA and Related Systems
• Proof-theoretic analysis of KPM
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
• Epsilon substitution method for theories of jump hierarchies
• Epsilon substitution method for -FIX
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Cut-elimination for impredicative infinitary systems part I. Ordinal-analysis for ID1
• Title not available (Why is that?)
• Title not available (Why is that?)
• Non-deterministic Epsilon Substitution Method for PA and ID 1
• Epsilon substitution for transfinite induction
• Zur Widerspruchsfreiheit der Zahlentheorie
• Title not available (Why is that?)

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}\)
• Title not available (Why is that?)

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)