 Hilbert thought that there can be no reasonable doubt about the soundness of classical Peano Arithmetic — or at least about the soundness of a subsystem of it that is called Primitive Recursive Arithmetic (Tait 1981). And he thought that every arithmetical statement that can be proved by making a detour through higher mathematics, can also be proved directly in Peano Arithmetic. In fact, he strongly suspected that every problem of elementary arithmetic can be decided from the axioms of Peano Arithmetic. Of course solving arithmetical problems in arithmetic is in some cases practically impossible. The history of mathematics has shown that making a “detour” through higher mathematics can sometimes lead to a proof of an arithmetical statement that is much shorter and that provides more insight than any purely arithmetical proof of the same statement.