A simple cut elimination proof for arithmetic with the epsilon symbol is used to establish the termination of a modified epsilon substitution process. This opens a possibility of extension to much stronger systems.

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 [W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie, Math. Ann. 117 162–194] succeeded in proving the termination of the process for the (...) first order arithmetic. In this note we report recent progress on the subject, and expound basic ideas of the epsilon substitution method à la Ackermann for the theory -FIX of non-monotonic inductive definitions. (shrink)

Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator εx. Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential (...) theorems obtained by this elimination procedure. (shrink)

The epsilon substitution method was proposed by D. Hilbert as a tool for consistency proofs. A version for first order predicate logic had been described and proved to terminate in the monograph “Grundlagen der Mathematik”. As far as the author knows, there have been no attempts to extend this approach to the second order case. We discuss possible directions for and obstacles to such extensions.