  How do Gödel’s theorems impact Hilbert’s program? Through a careful (“Gödel”-) coding of sequences of symbols (formulas, proofs), Gödel showed that in theories \(T\) which contain a sufficient amount of arithmetic, it is possible to produce a formula \(Pr(x, y)\) which “says” that \(x\) is (the code of) a proof of (the formula with code) \(y\).  Specifically, if \(\ulcorner 0 = 1\urcorner\) is the code of the formula \(0 = 1\), then \(Con_T = \forall x \neg Pr(x,\ulcorner 0 = 1\urcorner)\) may be taken to “say” that \(T\) is consistent (no number is the code of a derivation in \(T\) of \(0 = 1)\). The second incompleteness theorem (G2) says that says that under certain assumptions about \(T\) and the coding apparatus, \(T\) does not prove \(Con_T\). Now suppose there were a finitary consistency proof of \(T\). The methods used in such a proof would presumably be formalizable in \(T\). (“Formalizable” means that, roughly, if the proof uses a finitary operation \(f\) on derivations which transforms any derivation \(D\) into a derivation \(f (D)\) of a simple form; then there is a formula \(F(x, y)\) so that, for all derivations \(D,T \vdash F(\ulcorner D\urcorner ,\ulcorner f (D)\urcorner)\).) The consistency of \(T\) would be finitarily expressed as the general hypothetical that, if \(D\) is any given sequence of symbols, \(D\) is not a derivation in \(T\) of the formula \(0 = 1\). The formalization of this proposition is the formula \(\neg Pr(x,\ulcorner 0 = 1\urcorner)\) in which the variable \(x\) occurs free. If there were a finitary proof of the consistency of \(T\), its formalization would yield a derivation in \(T\) of \(\neg Pr_T (x,\ulcorner 0 = 1\urcorner)\), from which \(Con_T\) can be derived in \(T\) by simple universal generalization on \(x\). Yet, a derivation of \(Con_T\) in \(T\) is ruled out by G2.