[FOM] Harvey's first proof of Gödel's Second Theorem
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
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)
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
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
STEP TWO. Harvey now adds. "Note that we have proved  and  within 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
would prove a contradiction.
Whence, if PA is consistent, it can't prove Con(PA).
BUT HOLD ON .... Actually, we haven't, and Harvey hasn't, proved  and
 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/
More information about the FOM