I’m trying to think about how OLT would work if read, as is, by a student as a stand-alone text, as an introduction to its topics. That is, of course, a quite different issue from e.g. the question of how useful it will be to teachers to take and adapt chunks of the text and weave them into their own notes backing up a lecture course! So read the continuing comments in that light:
Part III: Computability (pp. 105-158) Ch. 9 is on Recursive Functions, and is reasonably clear but brisk (I think that non-mathematicians encountering this material for the first time will not find it easy and will need to read around in more discursive texts). Ch. 10 gives us 11 pages on the Lambda Calculus: this is surely either too much or too little. Almost nothing later depends on this, so the chapter can certainly be skipped. On the other hand, those baffled by the Lambda Calculus (in my experience, quite a few when they first encounter it, even among good maths students) will find this too quick to be terrifically helpful. An opportunity missed, perhaps.
Ch. 11 is rather different. This is a twenty-five page overview of Computability Theory getting as far as Rice’s Theorem: this is decently well done. Again I’m not sure there is enough detail for a first pass through this material: but I could recommend it as making useful revision material.
Part IV: Turing Machines (pp. 160-167). Chs. 12 and 13 are very short, and evidently awaiting considerable expansion.
Part V: Incompleteness (pp. 169-205). I have a horse in this race, of course, so am interesting to see how others canter down the track! Ch. 14 is on the Arithmetization of Syntax. It is difficult to do this stuff with a light touch, and (as elsewhere in OLT) I’d go for adding quite a lot more arm-waving motivation, here along the lines of “Look, consider the relation Pr(p, n) which holds when p codes for a well-formed proof in Q of the wff with number n. It’s easy to see that you can check whether Pr(p, n) without going in for any open-ended searches; here, informally, is how. So Pr is going to be primitive recursive, right?”. And since the chapter takes PA to be formalized in a sequent calculus, the details of arithmetization are inevitably a bit messy.
Ch. 15 is on Representability in Q. This is done the standard way, via the -function lemma, and we get out the undecidability of Q and hence of FOL. Then Ch. 16, Theories and Computability, shows that consistent extensions of Q are undecidable, and complete computably axiomatised theories are decidable — which together give us, in a familiar way, that consistent, computably axiomatized extensions of Q are incomplete. (Oddly, the undecidability of FOL is again proved along the way, without comment.) Ch. 17 then gives a more Gödelian proof of incompleteness via the fixed point lemma: it would perhaps have been good to say more about how this relates to the preceding proof. And then we have something pretty brisk on the Second Theorem and Löb’s Theorem. These chapters are reasonably clear. Stylistically, however, we are looking more at spruced-up (or not so spruced-up) notes rather than a discursive text: so they are not — I would have thought — as accessible or helpful to the beginner as a number of excellent treatments in the well-known literature.
Part VI: Sets, relations, functions (pp. 207-229). This is really an Appendix, the ‘little bit of set theory you need to know’, done at a very introductory level, getting as far as telling us about Cantor and non-enumerable sets. These pages are routine but clear enough. Naughtily, they tell us that functions are relations (Great Uncle Gottlob sighs, but he is used to this). Oddly, they introduce ordered pairs without tellings us how to represent them by sets, so there is something missing here. But this part is on its way to being a handy stand-alone module.
A general reflection on OLT. Having got to the end, it is clear that the different segments by different hands presuppose quite significantly different levels of sophistication from the reader. This makes me wonder a bit about the wisdom of presenting this resource as one long document rather than as a suite of separate modules. From the point of view of the rather daunted student, splitting things up would make it a lot clearer that you can and should pick and choose various parts, depending on your background and interests. But also dividing things into modules might encourage the potential contributor.
Logic teachers are a very picky lot with a tendency to think that other people’s books usually Do It Wrong (which is why we too often try to write our own)! So faced with one big text, most will find aspects to be pretty unhappy about, muttering “this just isn’t the best approach to getting this material across”. Suppose you think OLT is going about things the wrong way in Parts X and Z: then, at least speaking for myself, if you are therefore not really wedded to the overall book, you aren’t going to be very inclined to chip in to help improve Part Y (even if that is a part you rather like). So I wonder whether it would sell the project more strongly, be more enticing to students, and also encourage more potential contributors to various segments, if OLT were carved into quite separate modules?