Epsilon Substitution Method for 11 - CR: a Constructive Termination Proof
Sergei Tupailo · Logic Journal of IGPL · 2003
Following [1] and [2], we give a constructive cutelimination-style termination proof for Hilbert's epsilon substitution method for a theory Δ11 − CR, as defined in [3]. While the termination proof in [3] used second order reasoning and classical logic, our new proof is more in the spirit of ordinal analysis and is formalizable in HA + TI[α, Δ00], where α ≔ φ(ω, 0) = ‖Δ11 − CR‖ is the proof-theoretic ordinal of the theory. Familiarity with [2] and [3] is desirable.