Review of Three Views of Logic: Mathematics, Philosophy, and Computer Science by Donald Loveland, Richard Hodel, and S.G. Sterrett. Review #CR142187, Computing Reviews, April 17, 2014.

Mathematical logic historically had its roots in mathematics and philosophy, and it is one of the foundations of computer science. All three disciplines continue to contribute to the development of the field, and each provides a different perspective. The authors of this book --- Donald Loveland, a computer scientist; Richard Hodel, a mathematician; and Susan Sterrett, a philosopher --- have taught a multi-disciplinary course on logic for more than a decade; based on that course, they have now written this textbook.

The book is divided into three parts. Part I on proof theory covers propositional and predicate calculus, leading to most of a proof of the completeness of resolution theorem proving for predicate calculus (the remaining parts of the proof is in the exercises). There is a chapter and two appendices on Prolog, and appendices on induction and on Tarskian semantics for predicate calculus. Part II on computation theory covers register machines and recursion theory. Part III on philosophical logic covers Anderson and Belnap's relevance logic: its philosophical motivation, proof theory, and semantics.

The distinction between computer science and math in the first two parts is not very marked; as it happens part I on proof theory was written by the computer scientist and part II on computation theory by the mathematician, but it could just as easily have been the other way around. Overall, the material covered in these two parts is a little off the beaten track relative to most mathematical logic courses; in particular, the proof of completeness for resolution rather than for natural deduction, and the omission of both set theory and model theory.

As a computer scientist, I would have liked to have seen more computer science in the first two parts. The DPLL algorithm for satisfiability in the propositional calculus, which is very widely used in practice, is mentioned (the student is advised to Google it if interested) but not described; rather strangely, considering that author Donald Loveland is the second L of the algorithm name. There is no discussion of the state of the art in SAT-solving, in automated theorem proving, or in automated verification --- surely of interest to computer science students taking the course. The bad old tradition among theorists of writing algorithms with goto's rather than loops persists fifty years after Dijkstra's classic manifesto.

The third part is substantially off the beaten track of logic courses. I found it interesting from a technical standpoint. There is a very careful and readable account of how the rules for natural deduction proof in propositional relevance logic can be arrived at by restricting the power of rules for natural deduction in classical propositional logic, and an account of how this can be given a semantics in a four-valued truth system. I found it less satisfying from a philosophical and historical standpoint. The attitude toward Anderson and Belnap is rather worshipful; earlier work on relevance logic by Orlov, Ackermann, and Church, and earlier non-classical logics such as intuitionistic logic are not mentioned. Moreover the primary justification given here for preferring relevance logic to classical logic is that it is closer to usage in natural language. However, the book does not point out that, though the implication of relevance logic may be closer to the English "if/then" than material implication, it is not very close. "\$A \implies A \vee B\$" is valid in relevance logic (and every other logic I know of) but "If Paris is in France then either Paris is in France or Bambi is a gorilla" would be a very anomalous utterance. Whether a sentence in English involving "if/then" sounds reasonable involves many issues of pragmatics (in the linguistic sense) and will not be very adequately reflected in any symbolic logic.

All in all, for undergraduate logic students, there is certainly value in learning about resolution theorem proving and about non-classical logics; and if that is the material that an instructor wants to cover, this book is very well suited for the purpose.