[FOM] Proof of Godel's 2nd

[Harvey Friedman]

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. (Recall my earlier discussion of semantic forms of
Godel's second, on the FOM, which avoid proof predicates).

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