Is there a known natural model of Peano Arithmetic where Goodstein's theorem fails?

Question

(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.

Answer 1

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.

Answer 2

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.