Somewhat gappy Gödel

When planning and actually writing my Introduction to Gödel’s Theorems, I intentionally consulted other books as little as possible, trying to reconstruct strategies and proofs from memory as far as I could. I thought that would be a good discipline, and rethinking things through for myself would help me to explain things as clearly as possible. Well, people have indeed said nice things about the clarity of the resulting book, though my writing policy did mean I made a few nasty mistakes, some caught by pre-publication readers, and others corrected in later printings. I blush to recall ...

Anyway, now that I am working on a second edition, I want to spend the next month pausing to have a look at how others have handled the First Incompleteness Theorem. The basic shape of my book is fixed (after all, I’m doing another edition of IGT, not writing another different book, fun though that would be to do): but I might well get inspiration for how to make local improvements. So how do others state the Theorem? And how do they prove it? I’m planning to write up notes on expository themes and variations as I go along, and will post them here in due course.

The natural place to start is with Hilbert and Bernays. Slight problem: I don’t have German (yep, schoolboy Greek was all well and good, but hasn’t exactly been useful). Does anyone out there have detailed notes of how they prove the First Theorem in §5.1 of their second volume? I’d be really delighted to hear if so! Otherwise, there is a French translation, so I suppose I ought to do battle with that. Not that my French is any good these days either …

Until I can get hold of a translation of Hilbert and Bernays, then, the expository tradition for me will really have to start with Kleene’s wonderful 1952 Introduction to Metamathematics. I’m looking forward a lot to dipping into that again. Then I counted over forty other books on my shelves which give more or less detailed proofs of the First Theorem: hours of fun ahead, obviously. But I’ve started, yesterday and today, by rereading Gödel’s 1931 and his 1934 Princeton lectures. I have to blush again. I’d forgotten, for example, just what Gödel didn’t prove in 1931. ‘We shall only give an outline of the proof’ that every recursive relation is (as we would now say) representable in P;  ‘the entire proof’ [that for any predicate expressing a recursive property/relation there is an equivalent arithmetical predicate] ‘can be formalized in the system P‘ [it can be, no doubt, but this isn’t proved].

In fact, the situation is this. There are in fact two significantly different results stated in the 1931 paper, the ‘semantic’ and the ‘syntactic’ incompleteness theorems. The first requires that we are dealing with a theory which can express primitive recursive relations and is sound; the second version beefs up the first assumption and requires a theory which can represent p.r. relations while weakening the second assumption to require only that the theory satisfies the syntactic condition of omega-consistency. The first, ‘semantic’ theorem is sketched in Gödel’s §1, the official ‘syntactic’ version is the topic of the central §2 and §3. Look carefully, however, and while there is (enough material for) a full proof of the underplayed semantic version, the proof of the ‘syntactic’ result (the result that is normally meant when people talk now about the First Theorem) is in fact gappy, gappier than I’d really remembered.

Meanwhile, I see over 200 people have downloaded the draft of the first eight chapters of the second edition. Thanks to David Auerbach and Seamus Bradley for some amazingly speedy comments. Keep ’em coming folks!