It is known that if Peano's Arithmetic (PA)-which is a first order theory-is consistent, then Goodstein's theorem is an example of a sentence of PA that can be neither proved nor disproved in PA. Is it known whether this undecidability of Goodstein's theorem continues to hold in Z2-the standard axiomatizable theory of Second Order Arithmetic, whose axioms were first presented by Hilbert and Bernays?

  • $\begingroup$ Isn't it known that PA is consistent? ;) $\endgroup$
    – Alexey
    Oct 1, 2016 at 14:40

1 Answer 1


Yes, Goodstein's Theorem is provable in $Z_2$. Roughly speaking, this is because Goodstein's Theorem follows from the well-foundedness of $\epsilon_0$, and $Z_2$ can prove this. In fact, much less than $Z_2$ is needed: the theory $ATR_0$ is already more than enough.

EDIT: Thinking about Goodstein's theorem, and other similar results, leads natural to statements of the form $$\mbox{If $\alpha$ is well-ordered, then $F(\alpha)$ is well-ordered}$$ for some operation $F$ on linear orders. For Goodstein, the relevant map is $\alpha\mapsto \epsilon_\alpha$; note that $\epsilon_\alpha$ makes sense as a linear order, even if we can't prove it's well-founded.

NOTE: I'm not saying here that Goodstein is equivalent to the statement "If $\alpha$ is well-ordered, then so is $\epsilon_\alpha$" - the latter statement is much more general. Rather, the latter statement is a natural extension of Goodstein's theorem, and captures (I would argue) the "combinatorial intuition" contained in the theorem, even if it goes well beyond what is actually strictly needed.

We can then ask, as you do above, what axioms are needed to prove this result; this is the subject reverse mathematics. The reverse mathematics of such statements has recently been studied, e.g. by Montalban and Marcone in https://math.berkeley.edu/~antonio/papers/veblen.pdf. As it turns out, basically no operation $F$ which you can reasonably define, which sends ordinals to ordinals, requires us to go outside of $Z_2$. (This is partly reflected in the fact that the proof-theoretic ordinals for fragments of $Z_2$ much stronger than $\Pi^1_2$-$CA_0$ are completely out of reach, currently.)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.