Hilbert proposed the epsilon substitution method as a basis for consistency proofs. Hilbert's Ansatz for finding a solving substitution for any given finite set of transfinite axioms is, starting with the null substitution S0, to correct false values step by step and thereby generate the process S0,S1,… . The problem is to show that the approximating process terminates. After Gentzen's innovation, Ackermann 162) succeeded to prove termination of the process for first order arithmetic. Inspired by G. Mints as an Ariadne's (...) thread we formulate the epsilon substitution method for the theory ID1 of non-iterated inductive definitions for disjunctions of simply universal and existential operators, and give a termination proof of the H-process based on Ackermann 162). The termination proof is based on transfinite induction up to the Howard ordinal. (shrink)

We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.