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

Peter Smith ps218 at cam.ac.uk
Sat Apr 15 18:47:39 EDT 2006

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