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

William Tait wwtx at earthlink.net
Mon Apr 17 09:27:14 EDT 2006

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

More information about the FOM mailing list