[FOM] Goodstein's Theorem and Pi^1_1 comprehension
ali enayat
a_enayat at hotmail.com
Mon Apr 17 14:45:49 EDT 2006
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
More information about the FOM
mailing list