 Gödel’s incompleteness theorems showed that Hilbert’s optimism was undue. In September 1930, Kurt Gödel announced his first incompleteness theorem at a conference in Königsberg. Von Neumann, who was in the audience, immediately recognized the significance of Gödel’s result for Hilbert’s program. Shortly after the conference he wrote to Gödel, telling him that he had found a corollary to Gödel’s result. Gödel had found the same result already independently: the second incompleteness theorem, asserting that the system of Principia does not prove the formalization of the claim that the system of Principia is consistent (provided it is). All the methods of finitary reasoning used in the consistency proofs up till then were believed to be formalizable in Principia, however. Hence, if the consistency of Principia were provable by the methods used in Ackermann’s proofs, it should be possible to formalize this proof in Principia; but this is what the second incompleteness theorem states is impossible. Bernays also realized the importance of Gödel’s results immediately after he studied Gödel’s paper in January 1931, writing to Gödel that (under the assumption that finitary reasoning can be formalized in Principia) the incompleteness theorem show that a finitary consistency proof of Principia is impossible. Shortly thereafter, von Neumann showed that Ackermann’s consistency proof is flawed and provided a counterexample to the proposed \(\varepsilon\)-substitution procedure (see  Zach 2003).