(I've previously asked this question on the sister site here, but got no responses).

Goodstein's Theorem is the statement that every Goodstein sequence eventually hits 0. It turns out that this theorem is unprovable in Peano Arithmetic ($PA$) but is provable in $ZFC$.

I'd like to "discuss" this (both the proof in $ZFC$ as well as the proof that it's impossible in $PA$) in an hour long lecture to a group of grad students (with no assumed background, handwaving is not only allowed, but encouraged). Because of previous talks I've given, I think it will not take too long to cover/remind them of the basics of a semester course in first order logic (e.g., the compactness and completeness theorem, etc).

The problem is that the proofs of unprovability I've found (the same as those linked in the Wikipedia article) are rather too difficult for this setting. In a nutshell, I'm looking for the easiest known proof.

For example, I would love a proof of unprovability which works by exhibiting a model of $PA$ in which Goodstein's theorem fails. Such models neccesarily exist by the completeness theorem, since "$PA$ + Goodstein's theorem is false" is consistent.

Has anyone proven the independence of Goodstein's theorem by exhibiting a model of $PA$ where Goodstein's theorem has failed?

In the interest of getting as simple a proof as possible, I'd love to see a proof which uses the compactness and completeness ideas - something like showing there is a set $\Sigma = \{\phi_n\}$ of explicit first order sentences(in a slightly larger language, say) such that

1) for any finite $\Sigma_0\subseteq PA\cup \Sigma$, the standard model $\mathbb{N}$ models $\Sigma_0$ and

2) The theory $PA\cup \Sigma$ proves Goodstein's theorem is false.

Is such a proof known? More generally, is there a known proof of the unprovability of Goodstein's theorem which is accessible to someone with only a semester or 2 of logic classes?

Thank you and please feel free to retag as necessary.


2 Answers 2


Your proof strategy via (1) and (2) is impossible. If $PA\cup\Sigma$ proves that Goodstein's theorem is false, then the proof will have finite length, and so there will be some finite $\Sigma_0\subset\Sigma$ such that $PA\cup\Sigma_0$ proves that Goodstein's theorem is false. This would imply by (1) that Goodstein's theorem is false in the standard model. But Goodstein's theorem holds in the standard model, as Goodstein proved.

A second point is that you may find that there are no specific "natural" models of PA at all other than the standard model. For example, Tennenbaum proved that there are no computable nonstandard models of PA; that is, one cannot exhibit a nonstandard model of PA so explicitly that the addition and multiplication of the model are computable functions. (See this related MO question.) But I do not rule out that there could be natural nonstandard models in other senses.

  • $\begingroup$ I see - thank you for noticing what I should have already! $\endgroup$ Sep 1, 2010 at 0:07

I'm not sure I understand what you mean by "natural."

Anyway, the proof by Kirby-Paris is "model theoretic" or as "explicit" as you are likely to find. The reference is Accessible independence results for Peano arithmetic. Bulletin London Mathematical Society 14 (1982), 285–293. (I can email you the paper if you cannot find it easily. It is a nice read.)

The argument uses the method of indicators. The (very broad strokes) idea of the method is to start with a nonstandard model of PA (any would do, for some more specific results you may need to pay some attention to this step, but here any nonstandard model suffices), and use Goodstein's function $G$ (the map that assigns to $n$ the number of steps that the sequence takes to reach 0) to find a cut. This is an initial segment of your nonstandard model that is itself a model of PA, but the cut is built explicitly so that for some nonstandard $N$ in the cut the number of steps $G(N)$ is past the cut. This usually requires that you produce `indiscernibles' that are used to ensure the induction axioms hold in your cut. It is a very useful method, and the basis for most known independent results in PA. (The Paris-Harrington and Kanamori-McAloon theorems being other well-known examples).

I wrote a little paper showing that a well-known proof theoretic result about PA can be used to give the unprovability of Goodstein's theorem. The point of the paper is an explicit formula for $G$. You can find it in my page, or I can email it as well if you are interested.

  • $\begingroup$ Thank you for your response. I'll be sure you check out both your paper and the Kirby-Paris proof (I do have easy access to the paper). $\endgroup$ Sep 1, 2010 at 0:30
  • $\begingroup$ I didn't mean "natural" in any formal sense (and I can edit out the word or change it to a better one if you'd prefer). I meant "natural" in the sense of a model which could be used in a proof that Goodstein's theorem is independent of PA. I just needed some adjective to rule out models whose existence requires us to already know Goodstein's theorem is independent of PA (like the model guaranteed by Godel's completeness theorem applied to "PA + Goodstein's theorem is false"). $\endgroup$ Sep 1, 2010 at 0:32
  • $\begingroup$ Andres: A question about your paper. You say that your Theorem 1.9 is the main result of Wainer, "A classification of the ordinal recursive functions". Yet Wainer's paper does not mention Peano arithmetic or induction restricted to $\Sigma_k$ formulas. How do I see Theorem 1.9 in Wainer's notation? (It doesn't help that Wainer doesn't define the "Grzcgorczyk hierarchy" or "Peter's $k$-recursive functions".) $\endgroup$ Sep 8, 2010 at 13:43
  • $\begingroup$ Alright, I've now found a reference which does claim to prove the result you want. "Provably Computable Functions and the Fast Growing Hierarchy" books.google.com/… As yet, I can't understand the proof at all... $\endgroup$ Sep 8, 2010 at 17:31
  • $\begingroup$ Hi David, sorry I couldn't reply earlier, it's been terribly busy here today. Anyway, funny thing, I was going to suggest that you look at precisely the book you found, Logic and Combinatorics (Contemporary Mathematics, vol 65, AMS, 1987). Last I checked, it was still available through the AMS. It is a lovely book, really. There are some technical articles, and some very nice expository ones. The final article, by Steve Simpson, is a great introduction to the area of unprovability and combinatorics. The article by Buchholz and Wainer requires some familiarity with proof theory... $\endgroup$ Sep 8, 2010 at 23:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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