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

[Dmytro Taranovsky]

On Sun, 2006-04-16 at 15:33 -0500, 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.

ACA_0 is conservative over PA, and provably so in PRA.  Goodstein's
theorem is provable in the full ACA (and hence in ATR_0 and in
Pi^1_1-CA_0) and is equivalent over PRA to 1-Con (Sigma^0_1 soundness)
of PA.

Dmytro Taranovsky