  There has been some debate over the impact of  Gödel’s incompleteness theorems on Hilbert’s Program, and whether it was the first or the second incompleteness theorem that delivered the coup de grâce. Undoubtedly the opinion of those most directly involved in the developments were convinced that the theorems did have a decisive impact. Gödel announced the second incompleteness theorem in an abstract published in October 1930: no consistency proof of systems such as Principia,  Zermelo-Fraenkel set theory, or the systems investigated by Ackermann and von Neumann is possible by methods which can be formulated in these systems. In the full version of his paper,  Gödel (1931)  left open the possibility that there could be finitary methods which are not formalizable in these systems and which would yield the required consistency proofs. Bernays’s first reaction in a letter to Gödel in January 1931 was likewise that “if, as von Neumann does, one takes it as certain that any and every finitary consideration may be formalized within the system \(P\)—like you, I regard that in no way as settled—one comes to the conclusion that a finitary demonstration of the consistency of \(P\) is impossible”  (Gödel, 2003a,  87).