 This basic idea (the “Hilbertsche Ansatz”) was set out first by Hilbert in his 1922 talk (1923), and elaborated in lectures in 1922–23. The examples given there, however, only deal with proofs in which all instances of the transfinite axiom correspond to a single epsilon term \(\varepsilon x A(x)\). The challenge was to extend the approach to more than one epsilon term, to nested epsilon terms, and ultimately to second-order epsilons (in order to obtain a consistency proof not just of arithmetic, but of analysis).