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

[Andreas Weiermann]

Dear all,

perhaps the following remark is worth to state.

Let m^f_1:=m and m^f_{i+1}:=m^f_i[2+f(i) <-| 2+f(i+1)]-1
where the replacement of
base 2+f(i) through 2+f(i+1)
is in the complete base representation of m^f_i.
Then for f the identity function 

PA does not prove: forall m exists i m^f_i=0.

Let f_alpha(i):=log^{H^{-1}_\alpha(i)}
where log^k denotes k times iterated binary length and 
where the superscript -1 denotes inverse of a function
and H_\alpha is the alpha's level of the standard
Hardy hierarchy (classifying the PA provably rec.
functions).

Then for any \alpha<epsilon_0 

PA proves: forall m exists i m^{f_\alpha}_i=0

but 

PA does not prove: forall m exists i m^{f_{\epsilon_0}}_i=0.

This remark describes exactly the growth rate
in the base pumping 
for guaranteeing the unprovability
of the Goodsteinsequences.
The same threshold applies to the Hydra game
and to the Paris Harrington statement.

Best regards,
Andreas Weiermann