The Goodstein Sequence, or, using infinity to prove finitary results

I’d like to inaugurate this blog by demonstrating a wacky and somewhat radical proof technique.  If you feel threatened as you wade through a world of skeptics of infinity, I present to you your weapon.  It’s a cute little sequence of natural numbers called a Goodstein sequence.

In order to define this, we need a small amount of terminology.  Given a base n, we can write a number a in base-n notation as follows:

a = a_k n^k + a_{k-1} n^{k-1} + \dotsb + a_1 n + a_0,

where 0 \le a_i < n for all i.  For example, when a = 53 and n = 2, we have

53 = 2^5 + 2^4 + 2^2 + 1.

Hereditary base-n notation means that each of the exponents of n appearing in this expansion is also written in base-n notation, each of the exponents in the expansion of those exponents is also written in base-n notation, and so on.  In the above case, this looks like:

53 = 2^{2^2 + 1} + 2^{2^2} + 2^2 + 1.

Okay, here’s the Goodstein sequence G(a) starting with a number a.  Start by expressing a in hereditary base-2 notation; let’s call this stage 2.  To go from stage n to stage n+1, we do three things:

  • Increase all the n’s appearing in the hereditary base-n expansion to (n+1)’s.  This will give you a new number, written in hereditary base-(n+1) notation.
  • Subtract 1.  Just 1.
  • If necessary (if there was no n^0 term in the expansion of stage n), rewrite the number in hereditary base-n notation.

Here’s what we get if we start from

2^{2^2 + 1} + 2^{2^2} + 2^2 + 1 = 53.

Increase all the twos to threes and subtract one:

3^{3^3 + 1} + 3^{3^3} + 3^3 \approx 3^{28}.

Increase all the threes to fours and subtract one, noting that we have to rewrite the last term after subtracting:

4^{4^4 + 1} + 4^{4^4} + 3\cdot 4^3 + 3\cdot 4^2 + 3\cdot 4 + 3 \approx 4^{259}.

Play with this for a bit, or don’t.  Either way, you should be sufficiently shocked to learn the following:

Theorem (Goodstein).  Every Goodstein sequence converges to zero.

Before proving this, let me remark that this is still true, though slightly less shocking, for the analogous sequences in standard (non-hereditary) base-n notation.  That is, we write a number in base two, increase the twos to threes and subtract one, and so on, though now we’re not modifying the exponents when we change the base.  In particular, the only time the exponents change is when you subtract, changing the final term a_k n^k to (a_k - 1) n^k + (n-1) n^{k-1} + \dotsb + (n-1) n + (n-1).  Thus, for any term in the expansion, after enough steps, 1 will be subtracted from its coefficient and terms of lower exponents will be parachuted in to replace it.  In particular, the highest exponent in the expansion will eventually decrease, and by induction, the sequence will go to zero.

‘nm, just smoking dmt and adding pictures to math articles on wikipedia, u?’

This suggests that we want to somehow treat the bases that appear in the Goodstein sequence as placeholders.  The best way to do this, surprisingly, is to replace them all with ordinal numbers.  Given a number in hereditary base-n notation, one gets an ordinal number by replacing all the n’s in the expansion with \omega‘s.  It’s obvious that this defines an order-preserving injection from the natural numbers to the ordinal numbers.  Now let’s see what happens when we perform this operation on the Goodstein sequence above:

53 = 2^{2^2 + 1} + 2^{2^2} + 2^2 + 1 \mapsto \omega^{\omega^\omega + 1} + \omega^{\omega^\omega} + \omega^\omega + 1.

We now increase the base to three and subtract one, but note that the threes just become \omega‘s again:

3^{3^3 + 1} + 3^{3^3} + 3^3 \mapsto \omega^{\omega^\omega + 1} + \omega^{\omega^\omega} + \omega^\omega.

The next step kills the smallest power of four, and likewise replaces the smallest power of \omega with a finite sum of smaller ones (since only the fours, and not the smaller, ‘weaker’ coefficients and exponents created by subtraction, become \omega‘s):

4^{4^4 + 1} + 4^{4^4} + 3\times 4^3 + 3 \times 4^2 + 3 \times 4 + 3 \mapsto \omega^{\omega^\omega + 1} + \omega^{\omega^\omega} + 3\omega^3 + 3\omega^2 + 3\omega + 3.

In summary, the sequence of natural numbers becomes a strictly decreasing sequence of ordinals.  But the ordinals are well-ordered, so this sequence must (finitely) attain a fixed point.  Since 0 is the only fixed point of one of these operations, this fixed point must be zero, and thus the original sequence must converge to zero as well.

Oh, by the way, the same argument works not just for the sequence of bases 2,3,4,\dotsc, but for any non-decreasing sequence of natural numbers \ge 2.  This is what Goodstein originally proved.

What’s truly amazing about this is that the use of ordinal numbers isn’t just a helpful trick, it’s truly necessary to the proof, in the following sense:

Theorem (Kirby-Paris).  Goodstein’s theorem is not provable in Peano arithmetic.

What does this even mean?  (First, here’s Peano arithmetic, in case you’re unfamiliar; it’s a list of standard axioms that allow you to talk about induction, primality, divisibility, and various other important ideas about the natural numbers.)  Well, given any Goodstein sequence, if you sat down and calculated for long enough, you would in fact find that it converged to zero.  (Don’t do this!)  Thus, Peano arithmetic can prove Goodstein’s theorem for any given Goodstein sequence.  But the statement we want is about all Goodstein sequences at once, and the methods of Peano arithmetic are powerless to add this existential quantifier.  In fact, induction is basically the only way Peano arithmetic can prove statements about all of \mathbb{N}, and the argument above isn’t an induction argument at all.

The set-theoretic arguments made in Kirby and Paris’s paper are sadly out of my reach.  Here’s something of its basic structure, though.  First, note that the ordinals involved are all bounded by \epsilon_0.  Thus, we don’t need the whole of transfinite induction to make Goodstein’s argument, but a significantly weaker version called “quantifier-free transfinite induction up to \epsilon_0.”  (This is an axiom schema that says transfinite induction up to \epsilon_0 holds for any given formula with no bound variables — note that here we’re working with just one ordinal formula, so this quantifier-free version is sufficient.)  This was in Goodstein’s paper; Kirby and Paris show that Goodstein’s theorem is equivalent to quantifier-free transfinite induction below \epsilon_0.  Moreover, work of Gentzen shows that this axiom schema (plus Peano arithmetic) proves the consistency of Peano arithmetic.  Thus, if we had a proof of Goodstein’s theorem in Peano arithmetic, we would have a proof of the consistency of Peano arithmetic in Peano arithmetic.  By Gödel’s second incompleteness theorem, this is possible if and only if Peano arithmetic is inconsistent, which it isn’t, at least not in any model of set theory inhabited by decent, law-abiding folk.  Thus, Peano arithmetic can’t prove Goodstein’s theorem.

There’s a Java applet available that lets you play with Goodstein sequences.  A similar statement to Goodstein’s theorem, discussed in the Kirby-Paris paper linked above, involves a Hercules-and-the-hydra style game for which Andrej Bauer has a Java applet.  I’d welcome a better analysis of Kirby and Paris’s proof from anyone with a better understanding of set theory.  I’m also curious how bad this issue can get.  That is, are there statements formalizable in Peano arithmetic that are equivalent to transfinite induction up to higher ordinals than \epsilon_0?  Are there statements formalizable in Peano arithmetic that are equivalent to more drastic statements like the consistency of ZFC?  What about the Goodstein problem should lead one to expect a solution in a larger ‘set-theoretic world’, to speak informally?


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s