This book is an introductory course on formal logic at a college level. Although its authors are computer scientists, it is aimed at a broad audience, only requiring high school set theory and algebra.

It presents the basic material of propositional classical logic (syntax, semantics, and a few proof methods; chapters 1 to 5) and first-order quantified logic (chapters 6 to 10, 12), plus one chapter on induction. It is nice to have a book that can present such an important area as formal logic to a wide audience with so few prerequisites. For audiences with particular interest in computer science and the foundations of artificial intelligence, it would be nice to have some deeper mention of the recent advances on propositional SAT solvers [1] and the use of SAT as a model for complex problems [2,3].

An important innovation is the presence of online exercises with automated grading. There are also other online support materials.

The main innovation is in the presentation of the semantics of quantified first-order logic. Instead of the usual presentation based on Tarskian semantics, the book employs a Herbrand semantics. The reason claimed by the authors for that choice is simplicity, and thus being easier for students to understand. In fact, the notion of a Herbrand semantics is quite simple. One defines the Herbrand base as the set of all possible ground terms, and a model is simply a subset of that base. On the other hand, usual Tarskian semantics requires a much more complex notion of term interpretation.

Herbrand and Tarskian semantics provide the same expressivity on the relational level--that is, in the absence of functional symbols in the signature. This is not the case in the presence of functional symbols. First-order logic is compact with respect to Tarskian semantics, while compactness fails for Herbrand semantics. Still, the authors maintain that for an introductory approach, this simplicity far outweighs the deficiencies.

The authors do not make an important point with respect to logic as a knowledge representation tool. Herbrand semantics is an “inward looking” way to present first-order semantics, in the sense that the sentences are interpreted only in terms of the objects created by the signature. Tarskian semantics permit the elements of the logic to be interpreted with respect to any set (called a domain); that is, it gives the logic the representation power to “look outward” to any domain of application. While slightly more complicated, the Tarskian semantics highlights the expressivity of logic as a powerful representation tool.

Still, the proposal to consider Herbrand semantics at an introductory level has its appeal and it should be tested in the classroom. When a lecturer, or an interested student, decides to experiment with such an approach, this book is an excellent and carefully crafted support for that task.