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

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