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

[Andreas Weiermann]

Dear all,

Mathematical Reviews Proposes the following information

MR1011169 (90g:03058) 
Kent, Clement F.(3-LKHD); Hodgson, Bernard R.(3-LVL) 
Extensions of arithmetic for proving termination of computations. 
J. Symbolic Logic 54 (1989), no. 3, 779--794.

MR0687646 (84f:03049) 
Cichon, E. A. 
A short proof of two recently discovered independence results using
recursion theoretic methods. 
Proc. Amer. Math. Soc. 87 (1983), no. 4, 704--706.

The second paper is an elegant treatment of the standard results.
The first studies refinements where the growth rate involved
is sublinear instead of linear.

Optimal refinements can be gotten by the ordinal compression
technique. Roughly Termination of Goodstein is provable
for growth rate bound log^* but unprovable for growth
rate bound log_k (fixed iterate of the binary length function).

Best regards,
Andreas Weiermann