ABSTRACT
In fact, Hilbert’s epsilon substitution method, historically the first attempt at finding a finitary consistency proof for arithmetic, has a more semantic character. With this method one uses so-called epsilon terms to reduce arithmetic to a quantifier-free calculus, and then one looks for a procedure that assigns numerical values to any finite set of closed terms, in a manner consistent with the axioms. The first ordinal analysis of arithmetic using epsilon terms is due to Ackermann [i]; for further developments see, for example, [20].
