 In 1931 Gödel published a paper (1931a) that showed that there are true arithmetic statements that cannot be proved in the formal system of Principia Mathematica, assuming PM to be consistent. His methods not only applied to PM but to any formal system that contains a modicum of arithmetic. A couple of months after Gödel had announced this result at a conference in Königsberg in September 1930, von Neumann and Gödel independently realized that a striking corollary could be drawn from the incompleteness theorem. Every consistent and effectively axiomatized theory that allows for the development of basic parts of arithmetic cannot prove its own consistency. This came to be known as the second incompleteness theorem. (For details on these theorems and their history see  appendix A.4)  The second incompleteness theorem refutes the general ambitions of Hilbert’s program under the sole and very plausible assumption that finitist mathematics is contained in one of the formal theories of arithmetic, analysis or set theory. As a matter of fact, contemporary characterizations of finitist mathematics have elementary arithmetic as an upper  bound.[8]  In response to Gödel’s result, Hilbert attempted in his last published paper (1931b) to formulate a strategy for consistency proofs that is reminiscent of his considerations in the early 1920s (when thinking about the object theories as constructive) and clearly extends the finitist standpoint. He introduced a broad constructive framework that includes full intuitionist arithmetic and suggested extendibility of the new “method” to “the case of function variables and even higher sorts of variables”. He also formulated a new kind of rule that allowed the introduction of a new axiom \(\forall x A(x)\) as soon as all the numerical instances \(A(n)\) had been established by finitist proofs; in 1931 that is done for quantifier-free \(A(x)\), whereas in 1931b that is extended to formulae of arbitrary complexity. The semi-formal calculi, which articulate the broader framework, are based on rules that reflect mathematical practice, but also define the meaning of logical connectives. Indeed, Hilbert’s reasons for taking them to be evidently consistent are expressed in a single sentence: “All transfinite rules and inference schemata are consistent; for they amount to definitions”. Adding the tertium non datur in the form 