# [FOM] Harvey's first proof of Gödel's Second Theorem

Peter Smith ps218 at cam.ac.uk
Fri Dec 22 14:14:45 EST 2006

```Harvey advertises his argument as a proof of the *Second* Theorem for PA.
And his argument on the face of it doesn't involve all the usual hack work
of e.g. checking that the Hilbert-Bernays-Loeb derivability conditions hold
for PA. So this is great, if he's right. But let's look a bit more
carefully.

STEP ONE. We arithmetize "Turing machine index e, halts on input e", and
express that in PA using a sentence H(e). We then consider a Turing machine
that looks for a PA proof of not-H(e), and halts if it finds one, but
otherwise trundles on for ever. The Turing machine has index s, say, and we
ask the obvious question, does machine s halt on input s? I.e. is H(s)
true?

Then as Harvey notes, there are quick arguments which -- assuming (PA) is
consistent -- show that

1) H(s) is false, i.e. not-H(s) is true.
2) PA doesn't prove not-H(s).

We can also add, it is easy to show that -- assuming PA is omega-consistent
--

3) PA doesn't prove H(s) either.

But we can readily check that -- on the obvious construction --not-H(s) is
Pi_1. So putting (1), (2) and (3) together we get that, if PA is
omega-consistent, there is a true sentence of Goldbach type that PA can't
decide.

So far so good. But it also (isn't it??) fairly familiar. For example, a
generalized version is proved in Section 33.5 of my forthcoming
"Introduction to Goedel's Theorems" (CUP, about June: I've previously
posted drafts on the web, but CUP insist that I desist, now the book is
actually going through the press). I can't now recall from where -- if
anywhere -- I once upon a time got the proof; but my guess is that it is
folklore.

STEP TWO. Harvey now adds. "Note that we have proved [1] and [2] within PA
+ Con(PA)."

So if PA proved Con(PA), it would prove (1)•not-H(s), and hence it would
prove (1') PA proves not-H(s) [because if PA proves A, then PA proves that
PA proves A]. And it would also prove (2) PA doesn't prove not-H(s). So PA

Whence, if PA is consistent, it can't prove Con(PA).

BUT HOLD ON .... Actually, we haven't, and Harvey hasn't, proved [2] and
[1] within PA + Con(PA). The obvious quick arguments which Harvey sketches
are informal arguments. So his claim should be: his informal arguments
about Turing machines [which lead to the first theorem] can be formalized
in PA + Con(PA). [Compare the familiar claim that the usual arguments for
the first theorem can themselves be formalized in arithmetic, to give the
formalized first theorem PA |- Con(PA) --> not-Prov(G), i.e. PA + Con(PA)
|- not-Prov(G), which quickly yields the Second Theorem.]

Well, I'm sure that Harvey's implied claim that the informal arguments
*can* be formalized in PA + Con(PA) is dead right. But the question then
is: what exactly does it take to rigorously *check* that claim? Conjecture:
checking that this holds is as messy as checking that the HBL derivability
conditions hold, and involves the same kind of arguments.

I suspect, then, that Harvey's argument, cute though it is, only gives us a
novel take on the Second Theorem if my conjecture is false. (Of course, I'd
be very happy to be shown that it *is* false!!)

__________________________________________________________

Dr Peter Smith: Faculty of Philosophy, University of Cambridge

Goedel's Theorems: http://www.godelbook.net
LaTeX for Logicians: http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/

```