Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
From MaRDI portal
Publication:1399101
DOI10.1016/S0168-0072(02)00112-4zbMath1022.03040MaRDI QIDQ1399101
Publication date: 30 July 2003
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
transfinite inductionepsilon substitutiontermination proofHoward ordinalnon-iterated inductive definitionsordinal interpretation
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
This page was built for publication: Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)