2013

Continuing with a draft of the next section in the Big Books part of the Guide (see the previous post for more explanation):

Elliot Mendelson’s Introduction to Mathematical Logic (Van Nostrand, 1964: pp. 300) was first published in the distinguished and influential company of The University Series in Undergraduate Mathematics. It has been much used by generations of students since: a 4th edition was published by Chapman Hall in 1997 (pp. 440), with a slightly expanded 5th edition being published in 2009. I will here compare the first and fourth editions, as these are the ones I know.

This isn’t, in fact a very big Big Book: the length is kept under control in part by not covering a great deal, and in part by a certain brisk terseness. As the Series title suggests, the intended level of the book is upper undergraduate mathematics, and the book keeps to that aim. The style is indeed reasonably clear but though also now rather old-fashioned. (The choices of typography are not wonderfully pretty, and can make some pages look denser than they really are.)

After a brief introduction, Ch. 1 is on the propositional calculus. It covers semantics first (truth-tables, tautologies, adequate sets of connectives), then an axiomatic proof system. The treatments don’t change much between editions, and will only be of interest if you’ve never encountered a Hilbert-style axiomatic system before.

Ch. 2 is on quantification theory, again in an axiomatic style. The fourth edition adds to the end of the chapter more sections on model theory: there is a longish section on ultra-powers and non-standard analysis, then there’s (too brief) a nod to semantic trees, and finally a new discussion of quantification allowing empty domains. The extra sections in the fourth edition are a definite bonus: without them, there is nothing special to recommend this chapter, if you have worked through the suggestions in §1.1, and in particular the chapters in van Dalen’s book.

Ch. 3 is titled ‘Formal number theory’. It presents a formal version of first-order Peano Arithmetic, and shows you can prove some expected arithmetic theorems within it. Then Mendelson defines the primitive recursive and the (total) recursive functions, shows that these are representable (capturable) in PA. He then considers the arithmetization of syntax, and proves Gödel’s first incompleteness theorem and Rosser’s improvement. The chapter then proves Church’s Theorem about the decidability of arithmetic. One difference between editions is that the later proof of Gödel’s theorem goes via the Diagonalization Lemma; another is that there is added a brief treatment of Löb’s Theorem). If you’ve read my Gödel book or the equivalent, then there is nothing to divert you here, except that Mendelson does go through every single stage of laboriously showing that the relation m-numbers-a-PA-proof-of-the-sentence-numbered-n is primitive recursive.

Ch. 4 is on set theory, and — unusually for a textbook — the system presented is NBG (von Neumann/Bernays/Gödel) rather than ZF(C). In the first edition, this chapter is under fifty pages, and evidently the coverage can’t be very extensive and it also goes too rapidly. The revised edition doesn’t change the basic treatment (much) but adds sections comparing NBG to a number of other set theories. So while this chapter certainly can’t replace the introductions to set theory recommended in §1.7, it could be worth skimming briskly through the chapter in later editions to learn about NBG and other deviations from ZF.

The original Ch. 5 on effective computability starts with a discussion of Markov algorithms (again, unusual for a textbook), then treats Turing algorithms, then Herbrand-Gödel computability and proves the equivalence of the three approaches. There are discussions of recursive enumerability and of the Kleene-Mostowski hierarchy. And the chapter concludes with a short discussion of undecidable problems. In the later edition, the material is significantly rearranged, with Turing taking pride of place and other treatments of computability relegated to near the end of the chapter; also more is added on decision problems. Since the texts such as those by Cutland and Cooper mentioned in §1.6 don’t talk (much) about Markov or Herbrand-Gödel computability, you might want to dip into the chapter briefly to round out your education.

I should mention the appendices. The first edition has a very interesting appendix giving a version of Schütte’s variation on a Gentzen-style consistency proof for PA. Oddly this is missing from later editions. The fourth edition has instead an appendix on second-order logic.

Summary verdict There is now little reason to plough through the book end-to-end. It doesn’t have the charm and readability of Kleene 1952, and there are better separate introductions to each of the main topics. However, skim the early chapters if you’ve never seen axiomatic systems of logic used in earnest. Look at the section on non-standard analysis. If set theory is your thing, dip in to learn about NBG. And round out your knowledge of definitions of computation by looking through Ch. 5.

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.