[FOM] Re: Goodstein sequence is not provable in PA
Timothy Y. Chow
tchow at alum.mit.edu
Thu Apr 1 15:06:22 EST 2004
Jeff Hirst <jlh at cs.appstate.edu> wrote:
> Jhone asked:
> >Goodstein sequence is not provable in PA .Is that right? is there a
> >literature on this
> Yes and yes. Early papers on this include:
Perhaps someone here can clear up something that has confused me. If I
recall correctly, Goodstein's 1944 paper not only proved "Goodstein's
theorem" for an arbitrary "base-bumping function" (not just b |-> b+1),
but also the fact that this generalized version is unprovable in PA.
Much later, Paris and Kirby showed that the weaker statement (with the
specific base-bumping function b |-> b+1) is already unprovable in PA.
Or do I not have my facts straight?
Assuming that I have the facts right, then what puzzles me is that the
Paris-Kirby result, along with the Paris-Harrington Ramsey theorem, is
often advertised as the first "natural" finitary theorem to be shown to
be unprovable in PA. But doesn't this mean that the passage from an
arbitrary base-bumping function to a specific one is regarded as having
converted an unnatural theorem to a natural one? If so, why is this?
It doesn't seem to be that radical a difference to me.
Or maybe I've just been exposed to garbled advertisements.
More information about the FOM