(I've previously asked this question on the sister site [here](https://math.stackexchange.com/questions/3609/is-there-a-natural-model-of-peano-arithmetic-where-goodsteins-theorem-fails), but got no responses).


[Goodstein's Theorem](http://en.wikipedia.org/wiki/Goodstein%27s_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.



Is there a known natural model of Peano Arithmetic where Goodstein's theorem fails?
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](https://mathoverflow.net/questions/12426/is-there-a-computable-model-of-zfc).) But I do not rule out that there could be natural nonstandard models in other senses.


