  In  1926,  Hilbert introduced a distinction between real and ideal formulas. This distinction was not present in  1922b  and only hinted at in  1923.  In the latter, Hilbert presents first a formal system of quantifier-free number theory about which he says that “The provable formulae we acquire in this way all have the character of the finite” (1139). Then the transfinite axioms (i.e., quantifiers) are added to simplify and complete the theory (1144). Here he draws the analogy with the method of ideal elements for the first time: “In my proof theory, the transfinite axioms and formulae are adjoined to the finite axioms, just as in the theory of complex variables the imaginary elements are adjoined to the real, and just as in geometry the ideal constructions are adjoined to the actual” (ibid). When Hilbert, in  1926  explicitly introduces the notion of an ideal proposition, and in  1928,  when he first speaks of real propositions in addition to the ideal, he is quite clear that the real part of the theory consists only of decidable, variable-free formulas. They are supposed to be “directly capable of verification”—akin to propositions derived from laws of nature which can be checked by experiment  (1928,  475). The new picture of the program was this: Classical mathematics is to be formalized in a system which includes formalizations of all the directly verifiable (by calculation) propositions of contentual finite number theory. The consistency proof should show that all real propositions which can be proved by ideal methods are true, i.e., can be directly verified by finite calculation. (Actual proofs such as the \(\varepsilon\)-substitution had always been of such a kind: provide finitary procedures which eliminate transfinite elements from proofs of real statements, in particular, of \(0 = 1\).) Indeed, Hilbert saw that something stronger is true: not only does a consistency proof establish truth of real formulas provable by ideal methods, but it yields finitary proofs of finitary general propositions if the corresponding free-variable formula is derivable by ideal methods  (1928,  474).