[FOM] Re: Goodstein sequence is not provable in PA
Andreas Weiermann
weiermann at math.uu.nl
Tue Apr 6 14:10:27 EDT 2004
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
More information about the FOM
mailing list