 Ramsey’s theorem is a result in infinitary combinatorics, established by Frank Ramsey (1930), and deals with possibilities of “colouring” for certain graphs. Jeff Paris and Leo Harrington formulated a finitary variant of Ramsey’s theorem, and showed that it is not provable in PA (Paris &amp; Harrington 1977). This provides a quite natural statement of finite combinatorics which is independent of PA. Perhaps an even cleaner example is Goodstein’s theorem, due to Reuben Goodstein (1944), which is purely number theoretic in nature. First one defines a certain natural class of sequences of natural numbers, now called “Goodstein sequences”. The theorem states that every Goodstein sequence eventually terminates at 0. Goodstein’s theorem is certainly a natural mathematical statement, for it was formulated and proved (obviously by proof methods that go beyond PA) by Goodstein long before (that is, in 1944) it was shown, in 1982, that the theorem is not provable in PA (Kirby &amp; Paris 1982). 