 On the formalist view, a minimal requirement of formal systems of higher mathematics is that they are at least consistent. Otherwise every statement of elementary arithmetic can be proved in them. Hilbert also saw (again, dimly) that the consistency of a system of higher mathematics entails that this system is at least partially arithmetically sound. So Hilbert and his students set out to prove statements such as the consistency of the standard postulates of mathematical analysis. Of course such statements would have to be proved in a ‘safe’ part of mathematics, such as elementary arithmetic. Otherwise the proof does not increase our conviction in the consistency of mathematical analysis. And, fortunately, it seemed possible in principle to do this, for in the final analysis consistency statements are, again modulo coding, arithmetical statements. So, to be precise, Hilbert and his students set out to prove the consistency of, e.g., the axioms of mathematical analysis in classical Peano arithmetic. This project was known as Hilbert’s program (Zach 2006). It turned out to be more difficult than they had expected. In fact, they did not even succeed in proving the consistency of the axioms of Peano Arithmetic in Peano Arithmetic.