[FOM] Re: Goodstein sequence is not provable in PA

[Timothy Y. Chow]

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:
[refs deleted]

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.

Tim