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

[William Tait]

On Apr 16, 2006, at 5:30 PM, Aatu Koskensilta wrote:

> On Apr 16, 2006, at 11:33 PM, William Tait wrote:
>
>> 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.
>
> How can that be with ACA_0 (arithmetical comprehension + induction for
> sets) being conservative over PA? What am I missing?

Good grief, nothing. Peter Smith has already written to me privately,  
pointing out my blunder.

I hesitate to say anything for certain at the moment, but it does  
seem to be the case that the proof of Goodstein's theorem needs only  
PA+induction on epsilon_0.

Bill Tait