OK, after a bit of a gap, it is back to thinking about the Teach Yourself Logic self-study Guide. The shape of the Guide is evolving as I write it (well, at least there is random mutation …). I’m now inclined to carve the material into three main chunks. Ch. 1 will still be more or less the existing chapter on ‘The basics’ (as in the current edition, Version 7.1 from November, available here). Ch. 3 will be the already-promised chapter ‘Exploring further’ (of which only one section is so far on-line). But now, sandwiched between those chapters, I’m planning a chapter surveying the ‘Big Books’ on mathematical logic.
The usual menu for a first serious mathematical logic course is another treatment of first-order logic, basic model theory, basic theory of computability and related matters (like the incompleteness theorems), and introductory set theory. So the plan in this new Ch.2 will be to look at some of the single or dual author multi-topic books that aim to cover most or all of this menu, to give an indication of what they cover and — more importantly — how they cover it, while commenting on style, accessibility, etc.
It seems appropriate that this survey comes between Chs 1 and 3. For we will in fact be looking at further treatments of material already covered in some of the sections of Ch.1, keeping at the same or an only slightly more advanced level, without tackling some of the hairier excitements of Ch. 3. The survey books rarely provide the best introductions now available to this or that area: but they can provide useful aids to widening and deepening understanding and can be revealing about how topics from different areas can fit together.
I don’t promise to discuss every worthwhile Big Book, or to give even coverage to those I do consider. But I’m again working on the principle that a patchy guide is better than none at all. I’m going to take the Big Books in chronological order, so here — to get things started — is my draft section on the first on the list. This indicates the level of detail that I’m thinking of doing things in. Comments welcome as usual.
First published sixty years ago, Stephen Cole Kleene’s Introduction to Metamathematics (North-Holland, 1962: pp. 550) for a while held the field as a survey treatment of first-order logic, the theory of computable functions, and Gödel’s incompleteness theorems.
In a 1991 note about writing the book, Kleene notes that up to 1985, about 17,500 copies of the English version of his text were sold, as were more thousands of various translations (including a sold-out first print run of 8000 of the Russian translation). So this is a book with a quite pivotal influence on the education of later logicians, and on their understanding of the fundamentals of recursive function theory and the incompleteness theorems in particular.
But it isn’t just nostalgia that makes old hands continue to recommend it. Kleene’s book remains particularly lucid and accessible: it is often discursive, pausing to explain the motivation behind formal ideas. It is still a pleasure to read (or at least, it ought to be a pleasure for anyone interested in logic enough to be reading this far into the Guide!).
Chs. 1–3 are introductory. There’s a little about enumerability and countability (Cantor’s Theorem); then a chapter on natural numbers, induction, and the axiomatic method; then a little tour of the paradoxes, and possible responses.
Chs. 4–7 are a gentle introduction to the propositional and predicate calculus and a formal system which is in fact first-order Peano Arithmetic (you need to be aware that the identity rules are treated as part of the arithmetic, not the logic). Although Kleene’s official system is Hilbert-style, he shows that ‘natural deduction’ introduction and elimination rules can be thought of as derived rules in his system, so it all quickly becomes quite user-friendly. (He doesn’t at this point prove the completeness theorem for his predicate logic: as I said, things go quite gently!)
Ch. 8 starts work on ‘Formal number theory’, showing that his formal arithmetic has nice properties, and then defines what it is for a formal predicate to capture (‘numeralwise represent’) a numerical relation. Kleene then proves Gödel’s incompleteness theorem, assuming a Lemma — eventually to be proved in his Chapter 10 — about the capturability of the relation ‘m numbers a proof [in Kleene’s system] of the sentence with number n.
Ch. 9 gives an extended treatment of primitive recursive functions, and then Ch. 10 deals with the arithmetization of syntax, yielding the Lemma needed for the incompleteness theorem.
Chs. 11-13 then give a nice treatment of general (total) recursive functions, partial recursive functions, and Turing computability. This is all very attractively done.
The last two chapters, forming the last quarter of the book, go under the heading ‘Additional Topics’. In Ch. 14, after proving the completeness theorem for the predicate calculus without and then with identity, Kleene discusses the decision problem. And the final Ch. 15 discusses Gentzen systems, the normal form theorem, intuitionistic systems and Gentzen’s consistency proof for arithmetic.
Kleene writes beautiful clearly. And, modulo relatively superficial presentational matters, you’ll probably be struck by a sense of familiarity when reading through, as aspects of his discussions evidently shape many later textbooks (not least my own Gödel book). The Introduction to Metamathematics remains a really impressive achievement: and not one to be admired only from afar, either.
Summary verdict Still can be warmly recommended as an enjoyable and illuminating presentation of this fundamental material, written by someone who was himself so closely engaged in the early developments back in the glory days.