Abstract

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 α ≔ φ = ‖Δ11 − CR‖ is the proof-theoretic ordinal of the theory