[FOM] Goodstein's paper of 1944

[Alasdair Urquhart]

Goodstein's paper of 1944 is not really
on the subject of unprovability in PA,
but rather on the problem of expressing
Gentzen's induction on ordinals in 
finitist terms.  Goodstein begins by
expressing transfinite induction on 
ordinals up to epsilon_0 using numerical
sequences, and then remarks:

"The restricted ordinal theorem may now be
expressed by saying that ..." (p. 34).

In other words, Goodstein takes it for granted
that his formulation is an equivalent formulation
in finitist terms of induction up to epsilon_0.
However, he does not go on to show that his
encoding is (for example) provably equivalent in
PA to Gentzen's encoding, which would be required
for an independence proof -- presumably this could be done. 

He goes on to give a finitist proof of 
induction up to omega^omega, followed by 
some sketchy remarks about how it could be generalized.
He then says:

"The position appears to be, therefore, that if P(n)
expresses the restricted ordinal theorem for ordinals
less than [a finite stack of omegas], then P(n) is
capable of a finite construcive proof for *any assigned
n*, but (n)P(n) is not so provable ..." (p. 39)

So, I think the best that can be said is that Goodstein 
makes a plausible conjecture about an independence result
for PA.  Incidentally, one of the proofs in the paper is
by Bernays, and Goodstein expresses his "deep indebtedness
to Professor P. Bernays for much valuable advice and most
generous assistance."