************************
I offer the following proof of Godel's 2nd.
I define a particular TM related to PA thinking about TMs running at themselves. I run the TM at itself, and then everything follows very simply.
Thus the diagonalization is in the form of Turing machines running at themselves. Everything is seamlessly woven together, so that there is no separate self reference Lemma.
Will this make teaching Godel's 2nd easier? Or more fun?
Of course, since one is talking about unprovability of consistency, one cannot avoid the issue of having a decent proof predicate. That remains the subtle and awkward point. There is an earlier discussion of Godel's 1st and 2nd, where I give semantically based forms of Godel's 2nd that avoid the issue of a decent proof predicate. See
Opinions very welcome.
*******************************************
To make things as familiar as possible, we treat PA. We assume familiarity with Turing machines and their formalization in PA.
In particular, we will assume that every n >= 0 is the Godel number of a Turing machine. We write TM[n] for the n-th Turing machine.
We begin with the description of a particularly simple, fascinating(!) and diabolical(!) Turing machine TM.
At input n, TM searches for a proof in PA that "TM[n] does not halt at n". When it finds one, it immediately halts (and returns 0). Otherwise, TM will not halt.
Let TM be TM[k]. What if we run TM[k] at k?
case 1. There is a proof in PA that "TM[k] does not halt at k". Then TM[k] halts at k (by the action of TM = TM[k]). But then PA proves "TM[k] halts at k". Since PA is CONSISTENT, this case is impossible.
case 2. There is no proof in PA that "TM[k] does not halt at k". Then TM[k] does not halt at k (by the action of TM = TM[k]).
Note that we have proved
there is no proof in PA that "TM[k] does not halt at k". TM[k] does not halt at k.
within PA + Con(PA).
{These two lines alone, independently of their provability in PA + Con(PA), give us a form of Godel's 1st for PA}.
If PA were to prove Con(PA), then PA would prove
there is no proof in PA that "TM[k] does not halt at k". TM[k] does not halt at k.
From this, we see that PA would prove
there is no proof in PA that "TM[k] does not halt at k". PA proves "TM[k] does not halt at k".
Hence PA would be INCONSISTENT. QED
Furthermore, the entire argument takes place in a weak fragment of PA.
Harvey Friedman