This is a book on modal logic as it was in the 1980s, when I wrote my dissertation (and, probably, when the authors did as well). In the 1990s, I worked on modal logics to describe the behavior of computational structures. While reviewing this book, I wondered what it would have been like to have had it around at that time.

The authors express their annoyance with the view that modal logic amounts to rather simple-minded uses of two operators, ⋄ and □. Instead, they concentrate on more general results, and on the connection of modal logic to first-order logic, algebra, and computational complexity. Although they mention that prior acquaintance with first-order logic and its semantics is assumed, I would go further and demand prior acquaintance with the model theory of first-order logic. Ultrafilters, ultraproducts, and ultrapowers pop up everywhere, and if you don’t know how they work, the book might seem a bit intimidating.

Assuming such a background, some of the results proved in an accessible way here are the Jónsson-Tarski theorem (1952); Bull’s theorem (1966); the Goldblatt-Thomason theorem (1974); Sahlqvist’s theorems on correspondence and completeness (1975); Ladner’s theorem (1977); and van Benthem’s characterization of modal logic in classical logic (1983).

The core chapters are “Models,” “Frames,” and “Completeness,” supplemented by “Algebras,” and “Computation.” In a final chapter, the authors sketch more recent “Extensions,” such as the Sahlqvist theorem for the difference operator (1993), and a modal Lindström theorem (1995). These show once again the authors’ interest in explaining general results.

I think the book has a definite audience among logicians, but I want to focus upon its utility for computer scientists. I liked the treatment of bisimulation in the “Models” chapter, but was put off by the constant references to first-order logic.

In their recommendations for a course for computer scientists, the authors include the canonical results from the “Completeness” chapter, but not the sections on transforming the canonical model, the step-by-step method, and rules for the undefinable. Axiomatizations for semantically driven models require these techniques, and they are mentioned only briefly in treatments like Hughes and Creswell [1]. On the other hand, the last section, on Bull’s theorem, seems to fit in more with the “Frames” chapter.

The “Algebras” chapter seems a bit unmotivated. General frames are introduced as models and algebras rolled into one, whereas the intuition of Hughes and Cresswell [1], that general frames are between models and frames, in that they preserve substitution, seems more insightful.

The “Computation” chapter is excellent. I liked the sections on quasi-models and mosaics, and on undecidability, especially the three sections on NP, PSPACE and EXPTIME. From the last chapter, I enjoyed the treatment of the guarded and packed fragments of first-order logic.

To sum up, the book is good on what it promises to deliver, and useful to have as a reference. There are four appendices on necessary background, an excellent annotated and classified bibliography, and a decent index. The historical notes at the end of every chapter are also useful, although they tend to be slightly centered on Amsterdam. For instance, for all the authors’ lamenting over the neglect of algebra in modal logic, only a single mention is made of the work of Rasiowa, Sikorski, and their Polish school. The topological connections that they made from modal logic, extending the work of Stone, are not touched upon.

Fitting in with the book’s style, I would have liked to see the characterization of modal mu-calculus within monadic second-order logic by Janin and Walukiewicz [2], and as a convincing algebraic application, the completeness proof of modal mu-calculus via modal mu-algebras by Ambler, Kwiatkowska, and Measor [3].

For computer scientists, a book more oriented to their needs is necessary. For instance, those intending to learn about how to use modal logic to model their particular system need not bother with this book.

The authors wish to acknowledge and incorporate ideas from computer science, but this is mainly limited to propositional dynamic logic. Perhaps the main lesson to be learnt from computer science is that fragments of second-order logic are more important for its purposes than first-order logic. In particular, “second-order” behaviors generated from finite transition structures, and the connection to automata theory, are not addressed here. Where I felt the book was definitely dated is in the total absence of model checking: this has been a significant contribution of computer science to modal logic. The book by Huth and Ryan [4] is good on these aspects, although perhaps not general enough to suit the authors’ tastes.