Epsilon substitution method for elementary analysis (Q1908821)

The fundamental expression of the language on which the epsilon substitution method, introduced by Hilbert, is based, is \(\varepsilon xF[x]\), meaning ``an \(x\) satisfying the condition \(F[x]\)''. In such a context the existential and the universal quantifiers can be defined explicitly as follows: \(\exists xF[x] = F [\varepsilon xF[x]]\) and \(\forall xF[x] = F [\varepsilon x \neg F[x]]\), and the central axioms of the corresponding formalism are the so-called critical formulae having the following form \(F[t] \to F [\varepsilon x F[x]]\). Hilbert's basic idea to transform any (non-finitistic) number-theoretic proof into a finitistic proof by means of the substitution method was described in Grundlagen der Mathematik (Bd. 2) (by \textit{D. Hilbert} and \textit{P. Bernays}, see the new edition by Springer-Verlag (Berlin, 1970; Zbl 0211.00901)). The main problem in the realisation of this great idea, in the context of various mathematical theories, is to prove that the corresponding procedure terminates. In this paper, the authors formulate the epsilon substitution method for the second-order arithmetic with comprehension for arithmetical formulae with predicate parameters (i.e. for elementary analysis). Two essentially different proofs of termination are presented, the first of which, the constructive one, uses embedding into a ramified system of level one via cut-elimination, and the second, shorter and non-constructive one, uses a continuity argument. Due to the authors' nice style of presentation, this paper is very pleasant to read, although this subject, by definition, includes a lot of difficult and complex arguments and technical details.