[FOM] Re: Goodstein sequence is not provable in PA
weiermann at math.uu.nl
Tue Mar 30 14:14:24 EST 2004
Mathematical Reviews Proposes the following information
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.
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).
More information about the FOM