I’ve foolishly agreed to give a mini-mini-course on matters to do with incompleteness at a Cameleon weekend that Thomas Forster is organizing in four weeks time. I ought to find some new Deep and Interesting Things to say that aren’t in my book — but that’s a trifle difficult because if it was interesting and I knew it, I’d surely have put it in. I think I’m going to bluff my way through talking about iterated consistency extensions, but I need to do a lot more homework before I’ll feel comfortable, and at least the next two weeks are going to be very busy before I can really get round to that. Going to be a close-run thing!
Meanwhile, Arnon Avron has just been in touch with a rather embarrassing question about the book. Why didn’t I just point out that Theorem 30.10 (The truths of L, the language of arithmetic, aren’t r.e.) follows from Theorem 21.5 (given a sensible system of Gödel-numbering, no predicate of L can express the numerical property of numbering-a-truth-of-L).
Suppose for reductio there is a recursive function f that enumerates (the Gödel numbers for) the truths of L. Then we know that any recursive function can be expressed in L (put together Theorem 30.1 and the last remark in Sec 4.7). So in particular there is a formal wff F(x,y) which expresses the enumerating function f, and then by definition the formal wff Ex(Fx,y) will be satisfied by a number if and only if it numbers a truth of L. But then this is impossible by Theorem 21.5. Which proves Theorem 30.10.
Why the heck didn’t I say that? I guess I was so keen to make a connection with the informal proof in Ch. 5, and so motivate the discussion of Turing machines, that I forgot to mention the simple proof. Oops!