19
$\begingroup$

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?

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ 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. $\endgroup$
    – Lucas K.
    Commented Jun 24, 2013 at 18:09
  • 6
    $\begingroup$ 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$. $\endgroup$
    – François G. Dorais
    Commented Jun 24, 2013 at 18:26
  • $\begingroup$ 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. $\endgroup$
    – Lucas K.
    Commented Jun 25, 2013 at 18:39
  • $\begingroup$ 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. $\endgroup$
    – François G. Dorais
    Commented Jun 28, 2013 at 12:08
  • $\begingroup$ Perhaps this post is relevant: mathoverflow.net/q/354551/121665. $\endgroup$
    – Piotr Hajlasz
    Commented Oct 25, 2023 at 23:43

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented Jun 24, 2013 at 18:02
  • $\begingroup$ 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? $\endgroup$
    – Lucas K.
    Commented Jun 24, 2013 at 19:20
  • $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented Jun 24, 2013 at 21:34
  • $\begingroup$ See W. Buchholz and S.S Wainer "Provably Computable Functions and the Fast Growing Hierarchy", 1987 $\endgroup$
    – Kaveh
    Commented Jun 29, 2013 at 9:13

You must log in to answer this question.