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.