Mathematical logic is a challenging subject for many students. While its results are of critical importance to computer scientists, its experts often struggle to convey its main ideas to a lay audience. At first glance, this book, with its focus on the nature of proofs and algorithms and their relationship, appears to be targeted precisely for such an audience and should appeal to computer scientists and philosophers alike. However, it only delivers partially on its promise. The mathematical discussion is solid and rigorous, but there is little additional discussion that may help to explain some of the results to newcomers.

In essence, this book remains an introductory book on mathematical logic suited for a beginning graduate course in logic. It is written in the standard way one would expect from any textbook on mathematical logic: theorems and propositions are followed by proofs with very little commentary interspersed. Little space is provided for the discussions of additional motivations and applications, making the impact of the book’s ideas disappear behind the rigor.

The book is divided into three parts. Part 1, “Proofs,” contains chapters on predicate logic and models. The two chapters of Part 2, “Algorithms,” are titled “Computable Functions” and “Computation as a Sequence of Small Steps.” In Part 3, the relationship between proofs and algorithms is studied; it contains chapters on Church’s theorem, automated theorem proving, decidable theories, and constructivity. (The last two chapters (7 and 8) are very short and barely touch on their topics.) The book concludes with an epilogue in chapter 9 that very briefly summarizes the computer science applications of the topics discussed in earlier chapters.

This book can be recommended for a course on mathematical logic for an audience with sufficient mathematical background. Its conciseness makes it well suited for a one-semester graduate course. However, computer scientists and philosophers more interested in applications may want to look elsewhere.