  This sketch of the aims of the program was fleshed out by Hilbert and his collaborators in the following 10 years. On the conceptual side, the finite standpoint and the strategy for a consistency proof were elaborated by  Hilbert (1928);  Hilbert (1923);  Hilbert (1926)  and  Bernays (1928b);  Bernays (1922);  Bernays (1930),  of which Hilbert’s article “On the infinite”  (1926)  provides the most detailed elaboration of the finitary standpoint. In addition to Hilbert and Bernays, a number of other people were involved in technical work on the program. In lectures given in Göttingen  (Hilbert and Bernays, 1923;  Hilbert, 1922a),  Hilbert and Bernays developed the  \(\varepsilon\)-calculus  as their definitive formalism for axiom systems for arithmetic and analysis. Hilbert there also presented his approach to giving consistency proofs using his so-called \(\varepsilon\)-substitution method.  Ackermann (1924)  attempted to extend Hilbert’s idea to a system of analysis. The proof was, however, erroneous (see  Zach 2003).  John von Neumann, then visiting Göttingen, gave a corrected consistency proof for a system of the \(\varepsilon\)-formalism (which, however, did not include the induction axiom) in 1925 (published in  1927).  Building on von Neumann’s work, Ackermann devised a new \(\varepsilon\)-substitution procedure which he communicated to Bernays (see  Bernays 1928b).  In his address “Problems of the grounding of mathematics” to the International Congress of Mathematicians in Bologna in 1928  (1929), Hilbert optimistically claimed that the work of Ackermann and von Neumann had established the consistency of number theory and that the proof for analysis had already been carried out by Ackermann “to the extent that the only remaining task consists in the proof of an elementary finiteness theorem that is purely arithmetical.”