Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)

DOI10.1016/S0168-0072(02)00112-4zbMath1022.03040MaRDI QIDQ1399101

Toshiyasu Arai

Publication date: 30 July 2003

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

zbMATH Keywords

transfinite inductionepsilon substitutiontermination proofHoward ordinalnon-iterated inductive definitionsordinal interpretation

Mathematics Subject Classification ID

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

Related Items (11)

Epsilon substitution for \(ID_1\) via cut-elimination ⋮ Cut elimination for a simple formulation of epsilon calculus ⋮ Exact bounds on epsilon processes ⋮ 2006 Summer Meeting of the Association for Symbolic Logic: Logic Colloquium '06 ⋮ Epsilon substitution for transfinite induction ⋮ Ackermann's substitution method (remixed) ⋮ 2005 Annual Meeting of the Association for Symbolic Logic ⋮ Epsilon substitution method for -FIX ⋮ Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX ⋮ Epsilon substitution method for \([\Pi^0_1,\Pi^0_1\)-FIX] ⋮ The epsilon calculus and Herbrand complexity

Cites Work

• Unnamed Item
• Elementary induction on abstract structures
• Epsilon substitution method for theories of jump hierarchies
• Epsilon substitution method for elementary analysis
• Strong termination for the epsilon substitution method

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