Epsilon substitution method for ID1(Π10∨Σ10) Original Research Article

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 (Maths. Ann. 117 (1940) 162) succeeded to prove termination of the process for first order arithmetic. Inspired by G. Mints (draft June 1, 2000) as an Ariadneʹs thread we formulate the epsilon substitution method for the theory View the MathML source 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 (Maths. Ann. 117 (1940) 162). The termination proof is based on transfinite induction up to the Howard ordinal.