Ideas in the epsilon substitution method for -FIX

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 S 0 , to correct false values step by step and thereby generate the process S 0 , S 1 , … . The problem is to show that the approximating process terminates. After Gentzen’s innovation, Ackermann [W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie, Math. Ann. 117 (1940) 162–194] succeeded in proving the termination of the process for the first order arithmetic. s note we report recent progress on the subject, and expound basic ideas of the epsilon substitution method à la Ackermann for the theory Π 1 0 -FIX of non-monotonic Π 1 0 inductive definitions.