I have, for years and to largely underwhelmed ears, preached without portfolio the risk of treating connotation as denotation. So “first journey” in this book’s title indicated, to me, a not-especially-deep excursion into some selected subtopics of mathematical logic. Well, the depth and rigor of the treatment here were a positive but demanding surprise, given my “take”--and potentially yours--based solely on the title. I hasten to add that this is not a criticism, but rather an assessment of what a user--“reader” here would be too weak a word--of this just-short-of-200-page book can expect.

The authors’ stated aim: “to present a broad panorama of mathematical logic to students who feel curious about this field but have no intent to specialize in it.” Again, “broad” connotes, but of course does not denote “of limited depth,” which is emphatically not the case here. The authors accurately assert that their book is not a “comprehensive textbook, of which there already exist quite a few excellent ones.” In my view, it is certainly a textbook, among other things, as its substantial and substantive exercises are integral to it. And as such, it is, to say the least, excellent.

Another general observation, in the form of a difficult-to-falsify prediction: a nontrivial fraction of students who originally had no intention of specializing in logic will, as a result of the leg-up that this powerful book provides, in fact go into this field. If we continue with the journey metaphor, then we have six stops (chapters). (A cruise metaphor will not do, as several of these stops require an extended stay that is far too long to fit into that sort of excursion.) The six topics are:

- (1) Naive and Cantorian set theory, including orders, ordinal numbers and arithmetic; cardinal numbers and operations thereon; the axiom of choice.
- (2) First-order logic, including terms and formulas (syntax); semantics; formal proofs; Godel’s completeness theorem.
- (3) Model theory (first steps), including quantifier elimination.
- (4) Recursive functions, including Turing computable functions and recursively enumerable sets.
- (5) Models of arithmetic, including Peano arithmetic and Godel’s incompleteness theorems.
- (6) Axiomatic set theory, including Zermelo-Fraenkel theory and the von Neumann hierarchy.

By way of the proverbial full disclosure, I continue to assert my sympathies with constructivism and intuitionism, of which I found no coverage in this book--again, not a criticism, as the authors’ intentions are of limited scope. But the unparalleled precision, depth, and clarity of the book with respect to its covered topics will serve all computing professionals and fellow travelers (in addition to serving mathematicians of all stripes). I cut my teeth on axiomatic set theory and transfinite arithmetic, almost six decades ago, with Abian’s excellent book [1]. The first and last chapters of the present book are broader, deeper, and much more systematically formalized. The treatment, in chapter 1, of Cantor’s ordinal numbers and their cardinal evolutes is masterly, as is the explication of transfinite induction. Zermelo-Fraenkel (axiomatic) set theory (mostly) with choice (ZFC, chapter 6) is the best I’ve come across. (My fellow constructivists should know that the axiom of choice is a heavy hitter throughout this outstanding book that I nevertheless strongly urge you to read.)

Chapter 2, “First-Order Logic,” explicates “a standard way to formalize mathematics,” and will appeal in particular to computing scientists who are formal methodists. The treatments of syntax and semantics are worth the price of the book. Today’s broad categories of formal methods are syntactic (theorem-proving) and semantic (model-checking). Model theory is treated in chapter 3, which formalizes the notion of a theory itself.

The chapter (4) on primitive and general (computable) recursive functions features a multi-tape Turing machine that renders that abstraction’s operations clearer (to me) than those of the original, single-tape machine. There is a brief use of lambda notation to characterize functions, but no further elaboration of, or reference to, lambda calculus. The fact that not all recursively enumerable sets are recursive leads to the “undecidability of the halting problem and Rice’s theorem.” (In advocating formal methods to vice presidents in charge of safety-critical projects, I mention that the distance between theory and practice in high-assurance computing is zero. An interesting reference to Rice’s theorem can be found in Garoche’s *Formal verification of control system software* [2].)

Over the years, I’ve heard about Tarski’s famous post-Gödel undefinablity-of-truth-in-arithmetic theorem. Chapter 5, “Models of Arithmetic and Limitation Theorems,” provides a clear proof, as well as providing Church’s proof of the predicate calculus’s undecidability and Gödel’s incompleteness theorems.

This outstanding book will remain on my shelf indefinitely. The results derived therein are based on reliable (sometimes intricate) proofs that are built in well-defined, rigorous steps. It will be of great interest (also) to computing scientists and practitioners.