MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Goodstein's theorem is an example of a theorem that is not provable from first order arithmetic. All proofs of the theorem seem to deploy transfinite induction and I've wondered if one could prove the theorem without transfinite induction. Some time ago I came across this old usenet post where Torkel Franzen writes

Goodstein's theorem does not necessarily require transfinite induction for its proof, but it's not provable in elementary arithmetic. It can be proved by ordinary induction on a statement involving quantification over sets...

What is the proof/statement Franzen is referring to?

share|cite|improve this question
Note, that Goodstein can be proven in second order logic. So, if the sets are defined by predicates and you allow quantification over it, you have effectively a second order system. The proof in such system might however become close to the transfinite proof. – Lucas K. Jun 24 '13 at 18:09
Interesting! Have you checked Franzen's Inexhaustibility book? Sounds like this is a concrete way to see that $ACA_0$ with $\Sigma^1_1$-induction is not conservative over $PA$. – François G. Dorais Jun 24 '13 at 18:26
I have been thinking how exactly the second order proof goes. One should prove that if the exponents follow a well ordered relation, then the newly created relation is also well ordered. Which such proof, you can then do induction on the height of the exponent tower. Because, we are quantifying over all well ordered relations, this is a second order proof. In case of meta-logic (using Constructive omega rule), the quantification is on syntactical level. – Lucas K. Jun 25 '13 at 18:39
I'm out of the office so I can't check but Google books tells me there are four matches for "Goodstein" in the book (one of which is in the index). So I think it's worth a trip to the library. – François G. Dorais Jun 28 '13 at 12:08

I am quite convinced that Goodstein's theorem can be proven with the constructive omega rule. Or "meta-logic". For every individual 'n' Goodstein's theorem can be proven in elementary arithmetic (the problem is the quantification). In a meta-proof you can prove that for every 'n' such valid proof can be generated. I believe that this "meta-proof" only requires elementary arithmetic (if the meta-proof would require second order logic, then we wouldn't have achieved anything).

Of course, I can only claim this by detailing this out, but given my understanding of the Goodstein theorem, I am quite convinced that it should be possible.

share|cite|improve this answer
But the way that your prove it for each $n$ is essentially by transfinite induction up to the particular ordinal represented by replacing $2$ with $\omega$ in the complete base $2$ representation of $n$. The point is that PA is strong enough to prove that the corresponding relation is a well-order for each specific $n$ separately, but not that the full relation, corresponding to ordinal $\epsilon_0$, is a well-order. – Joel David Hamkins Jun 24 '13 at 18:02
Joel, I am not quite following your comment. As said, I am quite convinced that Goodman can be proven in FOL + PA + COR, (but it is a more than year ago that I have thought about it). Are you saying that this is incorrect or that this is similar to transfinite induction? – Lucas K. Jun 24 '13 at 19:20
I am saying that the proof in that system that I know is essentially the transfinite proof (but using codes for the ordinals as natural numbers). That is, to prove instance $n$ in PA, you in effect interpret $n$ as coding an ordinal, and use the fact that PA can prove that there is no infinite descending sequence of ordinals starting from that code. – Joel David Hamkins Jun 24 '13 at 21:34
See W. Buchholz and S.S Wainer "Provably Computable Functions and the Fast Growing Hierarchy", 1987 – Kaveh Jun 29 '13 at 9:13

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.