 Then Kurt Gödel proved that there exist arithmetical statements that are undecidable in Peano Arithmetic (Gödel 1931). This has become known as his Gödel’s first incompleteness theorem. This did not bode well for Hilbert’s program, but it left open the possibility that the consistency of higher mathematics is not one of these undecidable statements. Unfortunately, Gödel then quickly realized that, unless (God forbid!) Peano Arithmetic is inconsistent, the consistency of Peano Arithmetic is independent of Peano Arithmetic. This is Gödel’s second incompleteness theorem. Gödel’s incompleteness theorems turn out to be generally applicable to all sufficiently strong but consistent recursively axiomatizable theories. Together, they entail that Hilbert’s program fails. It turns out that higher mathematics cannot be interpreted in a purely instrumental way. Higher mathematics can prove arithmetical sentences, such as consistency statements, that are beyond the reach of Peano Arithmetic.