Goodstein Revisited
Thursday, June 2nd, 2005In the comments to Programming Language and Logic Links, citylight asked for an example of what proof theory is good for. I wanted to sketch an example using Goodstein sequences.
Proving that Goodstein sequences always eventually go to zero requires transfinite induction up to the ordinal \epsilon_0. Gentzen proved, using transfinite induction up to \epsilon_0, that Peano arithmetic was consistent. By Godel’s second incompleteness theorem, not consistent system can prove its own consistency, so transfinite induction up to \epsilon_0 is not expressible in Peano arithmetic, and Goodstein’s theorem is independent of it.
More details can be found at Fast Growing Functions and Unprovable Theorems.