This 29-chapter book covers the principal topics in logic and computability theory. In comparison with the second edition, chapter 28 on undecidable sentences and chapter 29 on the nonexistence of recursive nonstandard models of arithmetic are new. Chapters 26 and 27 have been revised, and other chapters contain new exercises.

To formalize the notion of computability, the authors define Turing machines, recursive functions, and “abacus computable functions.” They show that these definitions of computability are equivalent.

The authors discuss the important properties of first-order logic: completeness and soundness of a formalization of first-order logic, the compactness theorem, and the Skolem-Löwenheim theorem. They give a direct, surprisingly clear proof of the undecidability of first-order logic. The usual proof of undecidability is long and involved because it reduces to the undecidability of what the authors call “Robinson’s arithmetic.” Furthermore, the authors prove that all recursive (computable) functions are representable in Robinson’s arithmetic and, with this tool, they prove Gödel’s first incompleteness theorem and Tarski’s theorem on the indefinability of truth. The undecidability of first-order logic is a corollary of these results. The authors show that nonstandard models of arithmetic exist but recursive standard models do not exist.

The authors locate the precise boundary between decidability and undecidability of first-order logic. Monadic logic, which has only unary (one-argument) predicates among its nonlogical symbols, is decidable even in the presence of identity, whereas the logic without identity but with a single binary (two-argument) predicate is undecidable.

The authors demonstrate deep differences between first-order and second-order logics. For example, in contrast to Tarski’s theorem, arithmetical truth can be defined in second-order arithmetic. Other results include the Craig interpolation lemma, the Beth definability theorem, and Addison’s theorem on the nondefinability of the arithmetically definable sets.

The writing style is excellent: although many explanations are formal, they are perfectly clear. Modern, elegant proofs help the reader understand the classic theorems and keep the book to a reasonable length. Different parts of the book may be studied independently of each other.

The book is intended for advanced students “in philosophy of pure and applied mathematics who have mastered the material ordinarily covered in a first course in logic.” With the increasing influence of logic on the theory and practice of programming, this book will be very useful for graduate students in theoretical computer science.