The situation is the same for the statement Con(PA) expressing the consistency of PA. Gödel’s second incompleteness theorem shows that neither it nor its negation can be proved from PA but an appeal to some infinitary reasoning shows it to hold in the natural numbers. While perfectly fine for the logician’s need and central to the evaluation of Hilbert’s program, Gödel’s sentences appear concocted from the point of view of the practicing mathematician. Within Hilbert’s program statements of PA e