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

[Peter Smith]

Stephen Simpson's terrific SOSOA tells us that Pi^1_1-CA_0 [the theory in 
the hierarchy of subsystems of second-order arithmetic which allows 
comprehension for formula of the form \forall X phi (for arithmetic phi)] 
"is strong enough to develop a good theory of countable ordinal numbers". 
[p. 19]

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.

If that's right it's a bit surprising that it isn't noted in passing in the 
encylopedic SOSOA ... surprising enough for me to start worrying whether it 
*is* right! But it is, isn't it???

-- 
Dr Peter Smith: Faculty of Philosophy, University of Cambridge

Gödel's Theorems: http://www.godelbook.net 
LaTeX for Logicians: http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/ 
Idle musings: http://logicmatters.blogspot.com