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

[William Tait]

On Apr 15, 2006, at 5:47 PM, Peter Smith wrote:

> If I'm following here and later in the book, Pi^1_1-CA_0 therefore has
> enough ooph to prove Goodstein's Theorem. Which gives us a familiar  
> example
> of a first-order arithmetical statement unprovable in first-order  
> PA (and
> so unprovable in ACA_0) but provable in Pi^1_1-CA_0.

Note that, although Steve Simpson points out in his book a close  
model-theoretic relation between PA and ACA_0, the latter system is  
proof-theoretically stronger: Its proof-theoretic ordinal is epsilon_ 
{omega X 2}, I think---certainly it is at least epsilon_{omega}, as  
opposed to epsilon_0 for PA.

I haven't closely checked whether Goodstein's theorem is provable in  
ACA_0; but it seems from the exposition I have seen in Potter's book  
on set theory that it follows, using purely arithmetic reasoning by  
induction on epsilon_0.

Bill Tait