 Using the epsilon terms, quantifiers can now be eliminated from proofs in quantificational logic, thus transforming them into quantifier-free ones. Finally, the given derivation allows one, so it was conjectured, to determine numerical values for the epsilon terms. In his Leipzig talk of September 1922, published in 1923, Hilbert discussed this Ansatz for eliminating quantifiers and reducing the transfinite case to that of the quantifier-free theory. He presented the actual execution of this strategic plan only “for the simplest case” (in Hilbert 1923: 1143–1144). However, the talk was crucial in the development of proof theory and the finitist program: “With the structure of proof theory, presented to us in the Leipzig talk, the principled form of its conception had been reached”. That is how Bernays characterizes its achievement in his essay on Hilbert’s investigations of the foundations of arithmetic (1935: 204)