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

Andreas Weiermann weiermann at math.uu.nl
Tue Mar 30 14:14:24 EST 2004

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

More information about the FOM mailing list