[FOM] Re: Goodstein's Theorem and Pi^1_1 comprehension
Dmytro Taranovsky
dmytro at MIT.EDU
Mon Apr 17 11:53:00 EDT 2006
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
More information about the FOM
mailing list