[FOM] Goodstein's Theorem and Pi^1_1 comprehension

[ali enayat]

This is a reply to :

(a) A query of Peter Smith (April 15, 2006), who has asked whether 
Goodstein's theorem can be established within Pi^1_1-CA_0, and

(b) a remark of William Tait (April 15, 2006) about the possible provability 
of Goodstein's theorem in ACA_0.


Goodstein's theorem is already provable in ATR_0, an intermediate system 
between ACA_0 and Pi^1_1-CA_0.  One way of seeing this is to reduce the 
veracity of Goodstein's theorem to the sentence asserting the totality of 
the function H_(epsilon_0), where H_alpha is the alpha-th function in the 
Hardy hierarchy. (This was shown by E.A. Cichon, in Proc. Amer. Math. Soc., 
vol. 47, number 4 (1983), pp.704-706).

However, since ACA_0 is conservative over PA with respect to arithmetical 
sentences, Goodstein's theorem cannot be proved within ACA_0, since PA 
cannot prove the arithmetical sentence asserting the totality of  
H_(epsilon_0).

Best regards,

Ali Enayat