[Examples of] unprovable statements
After the appearance of Gödel's Theorem a variety of statements more or less directly related to provability were shown to be unprovable in Peano arithmetic and certain other axiom systems. Starting in the 1960s the so-called method of forcing allowed certain kinds of statements in strong axiom systems—like the Continuum Hypothesis in set theory (see page 1155)—to be shown to be unprovable. Then in 1977 Jeffrey Paris and Leo Harrington showed that a variant of Ramsey's Theorem (see page 1068)—a statement that is much more directly mathematical—is also unprovable in Peano arithmetic. The approach they used was in essence based on thinking about growth rates—and since the 1970s almost all new examples of unprovability have been based on similar ideas. Probably the simplest is a statement shown to be unprovable in Peano arithmetic by Laurence Kirby and Jeff Paris in 1982: that certain sequences g[n] defined by Reuben Goodstein in 1944 are of limited length for all n, where
g[n_] := Map[First, NestWhileList[{f[#] - 1, Last[#] + 1} &, {n, 3}, First[#] > 0 &]]
f[{0, _}] = 0; f[{n_, k_}] := Apply[Plus, MapIndexed[#1 k^f[{#2〚1〛 - 1, k}] &, Reverse[IntegerDigits[n, k - 1]]]]
As in the pictures below, g[1] is {1, 0}, g[2] is {2, 2, 1, 0} and g[3] is {3, 3, 3, 2, 1, 0}. g[4] increases quadratically for a long time, with only element 3×2402653211 - 2 finally being 0. And the point is that in a sense Length[g[n]] grows too quickly for its finiteness to be provable in general in Peano arithmetic.
The argument for this as usually presented involves rather technical results from several fields. But the basic idea is roughly just to set up a correspondence between elements of g[n] and possible proofs in Peano arithmetic—then to use the fact that if one knew that g[n] always terminated this would establish the validity of all these proofs, which would in turn prove the consistency of arithmetic—a result which is known to be unprovable from within arithmetic.
Every possible proof in Peano arithmetic can in principle be encoded as an ordinary integer. But in the late 1930s Gerhard Gentzen showed that if proofs are instead encoded as ordinal numbers (see note above) then any proof can validly be reduced to a preceding one just by operations in logic. To cover all possible proofs, however, requires going up to the ordinal ε0. And from the unprovability of consistency one can conclude that this must be impossible using the ordinary operation of induction in Peano arithmetic. (Set theory, however, allows transfinite induction—essentially induction on arbitrary sets—letting one reach such ordinals and thus prove the consistency of arithmetic.) In constructing g[n] the integer n is in effect treated like an ordinal number in Cantor normal form, and a sequence of numbers that should precede it are found. That this sequence terminates for all n is then provable in set theory, but not Peano arithmetic—and in effect Length[g[n]] must grow like [ε0][n].)
In general one can imagine characterizing the power of any axiom system by giving a transfinite number κ which specifies the first function [κ] (see note above) whose termination cannot be proved in that axiom system (or similarly how rapidly the first example of y must grow with x to prevent ∃y p[x, y] from being provable). But while it is known that in Peano arithmetic κ = ε0, quite how to describe the value of κ for, say, set theory remains unknown. And in general I suspect that there are a vast number of functions with simple definitions whose termination cannot be proved not just because they grow too quickly but instead for the more fundamental reason that their behavior is in a sense too complicated.
Whenever a general statement about a system like a Turing machine or a cellular automaton is undecidable, at least some instances of that statement encoded in an axiom system must be unprovable. But normally these tend to be complicated and not at all typical of what arise in ordinary mathematics. (See page 1167.)