Epsilon substitution method for ID₁(_1⁰ _1⁰)

DOI10.1016/S0168-0072(02)00112-4MaRDI QIDQ1399101zbMATH OpenFDO

Authors Toshiyasu Arai

Publication date 30 July 2003

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0168-0072(02)00112-4

zbMATH Keywords

epsilon substitutionHoward ordinalnon-iterated inductive definitionsordinal interpretationtermination prooftransfinite induction

Mathematics Subject Classification ID

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

Recommendations

• Epsilon substitution method for \([\Pi^0_1,\Pi^0_1]\)-FIX
• Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX
• Epsilon substitution method for -FIX
• Epsilon substitution for \(ID_1\) via cut-elimination
• Non-deterministic Epsilon Substitution Method for PA and ID 1
• scientific article; zbMATH DE number 6307937
• Epsilon Substitution Method for  11 - CR: a Constructive Termination Proof
• Epsilon substitution method for elementary analysis
• scientific article; zbMATH DE number 1870415
• Epsilon subdifferential method and integrability

Cites work

• Elementary induction on abstract structures
• Epsilon substitution method for elementary analysis
• Epsilon substitution method for theories of jump hierarchies
• scientific article; zbMATH DE number 1390268 (Why is no real title available?)
• Strong termination for the epsilon substitution method

Cited in

(21)

• A termination proof for epsilon substitution using partial derivations
• Epsilon substitution method for theories of jump hierarchies
• Epsilon substitution for \(ID_1\) via cut-elimination
• Epsilon substitution for transfinite induction
• Epsilon substitution for first- and second-order predicate logic
• Cut elimination for a simple formulation of epsilon calculus
• Ackermann's substitution method (remixed)
• Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX
• Epsilon substitution method for \([\Pi^0_1,\Pi^0_1]\)-FIX
• Hilbert's ‘Verunglückter Beweis’, the first epsilon theorem, and consistency proofs
• Epsilon substitution method for -FIX
• scientific article; zbMATH DE number 4108755 (Why is no real title available?)
• Epsilon Substitution Method for  11 - CR: a Constructive Termination Proof
• scientific article; zbMATH DE number 1870415 (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?)
• Exact bounds on epsilon processes
• 2006 Summer Meeting of the Association for Symbolic Logic: Logic Colloquium '06
• 2005 Annual Meeting of the Association for Symbolic Logic
• Non-elementary compression of first-order proofs in deep inference using epsilon-terms
• The epsilon calculus and Herbrand complexity

This page was built for publication: Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)

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