Modern Mathematical Logic is a strong addition to the niche occupied by books like Enderton’s classic $\boldsymbol {A \ Mathematical \ Introduction \ to \ Logic}$ (third edition: Academic Press, 1972)—a book introducing first-order logic to mathematics students at the later undergraduate or early graduate level, while laying the groundwork for a possible future course in more specialized topics in logic.

It combines clear explanations and motivation with careful handling of the technical details, accompanied by lots of examples. It’s much longer than, for instance, Enderton, primarily because it includes a great deal of side material introducing topics in various parts of logic—it’s the right amount of too much for a semester course, enough to introduce the core theorems of first-order logic and then have a selection of topics to choose from to fill out the semester.

The book opens with a formal development of induction and recursion followed by a chapter on the syntax and semantics of propositional logic. This can be challenging to teach since parts of the material are familiar to many students, but not always in a way that prepares them for what’s to come. Mileti digs into the complexity, presenting a proof system along with proofs of soundness, completeness, and even compactness as warm-ups for what will follow. This means there’s enough new material to keep the attention of students for whom truth tables are routine.

The analogous results for first-order logic occupy three of the next four chapters, with an interlude for some elementary model theory. The book then develops some topics in, as the title promises, modern mathematical logic—model theory, set theory, and computability theory.

The model theory part stands out as the strongest of the introductions to parts of logic, both in depth and in establishing the sense that there are further interesting developments to be explored beyond the book—various sections introduce the spectrum of a theory, the random graph, nonstandard analysis, quantifier elimination for algebraically closed fields, and ultraproducts, most of these as standalone bits one can cover or not as desired.

The introduction of the axioms of ZFC is a highlight of the book, introducing them slowly and motivating the more challenging ones in some detail. The remainder of the set theory section is less an introduction to set theory as a field, and focuses on the development of ordinals and cardinals one might want, for instance, as preparation for a model theory or computability theory course which will need real use of transfinite induction.

The computability theory section is integrated into the buildup to the final chapter, which at last proves the first incompleteness theorem and states (and proves, modulo the usual technical assumptions about encoding) the second incompleteness theorem.

The technical part of the incompleteness theorem—the introduction of the primitive recursive and recursive functions and the corresponding coding machinery—is quite well done and fits well with the book’s overall rather computational style. (One has to decide, of course, how much to actually dig into the long string of technical lemmata about encodings and how much to just admire that they’re present.) The book briefly introduces a notion of register machine and discusses the Church–Turing thesis, though it feels a bit too cursory for students without some background in computer science. Finally, there’s one brief section introducing the idea of computably enumerable sets, but, unfortunately, the book stops before introducing Turing degrees or the arithmetical hierarchy.

The book mostly assumes no particular mathematical background outside some (usually well-marked) exercises. The one exception is around the Löwenheim–Skolem theorem, where facts about cardinality are unavoidable. Modern Mathematical Logic handles this by initially only showing downward Lowenheim–Skolem for countable theories (reviewing the necessary facts about countable sets quickly in an appendix, probably too quickly for students seeing the topic for the first time), and pushing the full theorem off until cardinals have been developed in a more formally set-theoretic context.

The book is replete with examples and motivation, but still feels a bit dense. The proofs tend towards a formal syntactic style that feels a little like executing computer programs. In some places this works well, but in others, the formality seems more technical than useful. For instance, the definition of the language of first-order logic culminates by defining the formulas of the language $\mathcal {L}$ to be

$$\begin{align*}G(\mathrm{Sym}^*_{\mathcal{L}},\mathrm{AtomicForm}_{\mathcal{L}}\cup\{\top,\bot\},\{h_\neg,h_\wedge,h_\vee,h_{\rightarrow}\}\cup\{h_{\forall,x},h_{\exists,x}\mid x\in\mathrm{Var}\}). \end{align*}$$

For students from computer science backgrounds, this can work, but from a more purely mathematical or, especially, philosophical background, this has turned into pure technical computation without meaning.

The proof system used has some serious issues. It starts promisingly, using a natural deduction system in sequent form (that is, one tracks open assumptions on the left hand of a turnstile) and linearized (so a deduction is a sequence, not a tree)—overall a good balance between intuition and technical benefits. In keeping with the book’s tendency towards computational formality, the sequents are sequences rather than sets, requiring various fidgeting with structural rules. The rules, though, are chosen haphazardly; for instance, the $\vee $ elimination rule is asymmetric (from $S\vdash \phi \vee \psi $ and $S\vdash \neg \phi $ , one can infer $S\vdash \psi $ ), and one needs double negation elimination to infer the other direction. The result is both pointlessly difficult to prove things in (the erratic choice of rules breaks the usual backwards reasoning that works so well in natural deduction) and inapplicable (for instance, the presence of structural rules would be worthwhile if one were going to consider the possibility of substructural logics, but the rules are so strange that not even intuitionistic logic is a subsystem).

These flaws mean that Modern Mathematical Logic is not quite the perfect logic book, but it’s a very good one. As the praise on its cover from many logicians (including me) suggests, it is likely to become a new standard for such courses.