 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 expressible either without quantifiers or with a string of universal quantifiers followed by a non-quantificational formula count as finitistic statements. The statements \(G\) and Con(PA) mentioned above also belong to this class. Finitistic statements with obvious mathematical relevance include basic properties such as the commutativity of addition as well as the statement of Fermat’s last theorem (whose proof has been established using higher mathematics but logicians are convinced that it can also be carried out in PA). Logicians have not been able to find finitistic statements with obvious mathematical significance that require a detour through the infinite, but they have been able to do the next best thing. They have found statements that have the form \((\forall x) (\exists y) A(x, y),\) which express a certain functional connection between numbers and have shown that such statements, although true, cannot be proved using only the resources of PA. Among the most famous such results are a modification of Ramsey’s finite theorem provided by Paris and Harrington (1977), and the proof that a theorem by Goodstein (1944) cannot be proved in PA (Kirby and Paris 1982).  There are stronger results that are independent of even stronger systems that are studied within the context of reverse mathematics (e.g., Kruskal’s theorem is independent of predicative analysis—see Simpson 1985, 2002).