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

[Peter Smith]

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 
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 [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/