 Similar broadly constructivist tendencies were also very much in evidence in the proof theoretical work of Hilbert and Bernays and their followers in the 1920s. Already by the time of Hilbert’s 1921/22 lectures Hilbert had identified the introduction of the (classical) quantifiers as the crucial step where the transfinite entered logic. Hilbert, like C. S. Peirce long before, thought of the quantifiers as infinite conjunctions and disjunctions, and from the early 1920s onwards it was well understood in Göttingen that, for the programmatic goals of the Hilbert consistency program to be carried out, a finitary analysis of the quantifiers was necessary. The epsilon-substitution method was the principal device Hilbert introduced in order to attempt to attain this result. (A survey of this research is provided by Sieg 2009 and in the introductory notes to Hilbert [LFL].)