Modal logic.

*(English)*Zbl 0988.03006
Cambridge Tracts in Theoretical Computer Science. 53. Cambridge: Cambridge University Press. xxii, 554 p. (2001).

This textbook on modern propositional modal logic is exceptional in every respect. The exposition of the subject is very clear and careful. The eloquent and didactically experienced authors succeed in exciting the reader’s curiosity and guiding her/him on her/his way to (and through) the crucial points, always providing the right degree of support.

The book is divided into seven chapters, preceded by a preface that puts the reader in the right mood for dealing with modal logic, at least for a while. Each chapter starts out with a ‘chapter guide’ introducing the contents of the respective sections. Moreover, all sections are assigned to either the ‘basic track’ (the major part of a chapter each time) or the ‘advanced track’. Several exercises make up an essential part of every section. After the subject of a chapter has been presented, a ‘summary’ orders the material once again with regard to the newly treated ideas and methods. Concluding a chapter, detailed notes are given concerning references and related topics.

Four appendices follow the main part of the book, supplying the reader with background material from logic, algebra and computer science, and a guidance on further reading, respectively, which is well received not only because it is always kindly disposed towards the works referred to. The book is concluded by an extensive bibliography, a nicely structured list of notation, and an exhaustive index.

The headings of the individual chapters read as follows: Basic concepts – Models – Frames – Completeness – Algebras and general frames – Computability and complexity – Extended modal logic. In the following, we rather touch on some of the topics treated there than report the complete content (not even all of the highlights). – The fundamental approach of the book, viz viewing modal logic as a logic of relational structures, is developed in the introductory chapter. Basic modal and tense logic, arrow logic, and propositional dynamic logic, serve as the standard examples of the different shaping of modal logic here (and later on as well). The first chapter contains also a broad historical overview. – The second chapter focuses on modal model theory. In this context the key idea is bisimulation, subsuming many of the model-connecting means studied in modal logic earlier. Van Benthem’s characterization of the modal fragment of first-order logic is presented as the first result on the advanced track. – The third chapter is mainly about modal definability and correspondence theory. In particular, the famous Sahlqvist Correspondence Theorem is proved. – Much of the efforts made in modal logic revolved around completeness. Several methods for proving completeness are explained and applied in the midchapter of the book, in particular, to the sample logics mentioned above. – The next chapter deals with algebraic modal logic. The Jónsson-Tarski Theorem and the Sahlqvist Completeness Theorem are proved, among other things. Furthermore, the part general frames play in modal logic is made clear. – The penultimate chapter takes the significance of modal logic for computer science into account. Several techniques for proving (un)decidability are exemplified, and the particularly relevant complexity classes NP, PSACE and EXPTIME are examined modally. – Some extensions of modal logic are treated in the final chapter of the book, including hybrid logic, the guarded fragment, and multi-dimensional modal logic.

The book is aimed at (and actually suited to) a widespread target group ranging from students to researchers, from logicians to linguists. In our opinion, it is useful especially for people working in (fields related to) computer science (although implementation-oriented modal proof theory is omitted deliberately). The main point of the book, however, is this: the beauty of modal logic becomes apparent, over and above all the various areas of application.

The book is divided into seven chapters, preceded by a preface that puts the reader in the right mood for dealing with modal logic, at least for a while. Each chapter starts out with a ‘chapter guide’ introducing the contents of the respective sections. Moreover, all sections are assigned to either the ‘basic track’ (the major part of a chapter each time) or the ‘advanced track’. Several exercises make up an essential part of every section. After the subject of a chapter has been presented, a ‘summary’ orders the material once again with regard to the newly treated ideas and methods. Concluding a chapter, detailed notes are given concerning references and related topics.

Four appendices follow the main part of the book, supplying the reader with background material from logic, algebra and computer science, and a guidance on further reading, respectively, which is well received not only because it is always kindly disposed towards the works referred to. The book is concluded by an extensive bibliography, a nicely structured list of notation, and an exhaustive index.

The headings of the individual chapters read as follows: Basic concepts – Models – Frames – Completeness – Algebras and general frames – Computability and complexity – Extended modal logic. In the following, we rather touch on some of the topics treated there than report the complete content (not even all of the highlights). – The fundamental approach of the book, viz viewing modal logic as a logic of relational structures, is developed in the introductory chapter. Basic modal and tense logic, arrow logic, and propositional dynamic logic, serve as the standard examples of the different shaping of modal logic here (and later on as well). The first chapter contains also a broad historical overview. – The second chapter focuses on modal model theory. In this context the key idea is bisimulation, subsuming many of the model-connecting means studied in modal logic earlier. Van Benthem’s characterization of the modal fragment of first-order logic is presented as the first result on the advanced track. – The third chapter is mainly about modal definability and correspondence theory. In particular, the famous Sahlqvist Correspondence Theorem is proved. – Much of the efforts made in modal logic revolved around completeness. Several methods for proving completeness are explained and applied in the midchapter of the book, in particular, to the sample logics mentioned above. – The next chapter deals with algebraic modal logic. The Jónsson-Tarski Theorem and the Sahlqvist Completeness Theorem are proved, among other things. Furthermore, the part general frames play in modal logic is made clear. – The penultimate chapter takes the significance of modal logic for computer science into account. Several techniques for proving (un)decidability are exemplified, and the particularly relevant complexity classes NP, PSACE and EXPTIME are examined modally. – Some extensions of modal logic are treated in the final chapter of the book, including hybrid logic, the guarded fragment, and multi-dimensional modal logic.

The book is aimed at (and actually suited to) a widespread target group ranging from students to researchers, from logicians to linguists. In our opinion, it is useful especially for people working in (fields related to) computer science (although implementation-oriented modal proof theory is omitted deliberately). The main point of the book, however, is this: the beauty of modal logic becomes apparent, over and above all the various areas of application.

Reviewer: Bernhard Heinemann (Hagen)

##### MSC:

03-02 | Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations |

03B45 | Modal logic (including the logic of norms) |

68Q15 | Complexity classes (hierarchies, relations among complexity classes, etc.) |

03B25 | Decidability of theories and sets of sentences |

03B70 | Logic in computer science |