Modal logic has been widely used in computer science since it was realized that Kripke’s possible world semantics can model transition systems, in which our subject abounds. Computer science has also contributed to logic, by translating structured transition systems into dynamic logic. However, most work deals with propositional modal logics. Modal predicate logic is full of philosophical pitfalls, such as Frege’s morning star/evening star puzzle.
In this monograph, Fitting and Mendelsohn give a clean treatment of first-order modal logic. After three introductory chapters on propositional modal logics, the next five chapters show that first-order logic with relational symbols (including equality) poses no special problems. Both possibilist (over objects in all possible worlds) and actualist (over objects in the world where the formula is being checked for truth) quantifiers are treated. The focus of the book is on actualist quantifiers, which have proven more difficult to handle. The proof machinery is through semantic tableaus, and soundness and completeness are carefully proven for the basic modal logic K.
The next two chapters deal with the fundamental question of how terms are to be handled. For instance, are constants rigid? That is, do they designate the same object in all worlds? Once again, the more general choice of non-rigidity is followed in this book. But now, the authors ask, for the formula ⋄ P ( t ), is the term t to be evaluated in the current world, or in the one whose possibility is being talked of? For example, in the sentence “On India’s independence, the prime minister said it was a tryst with destiny,” are we referring to the prime minister then, or the prime minister of today?
Since both choices make sense in different contexts, the authors propose a scoping mechanism: the two choices can be expressed by ⋄ ( &lgr; x ∽ p m ) Twd ( x ) and ( &lgr; x ∽ p m ) ⋄ Twd ( x ), where ⋄ refers to the time of independence, and Twd refers to the prime minister’s speech. The syntax used in the book is restricted so that terms and predicates interact only through variables. For instance, R ( t1 ,..., tn ) is not allowed. But this is easy to rectify: translate it to ( &lgr; x1 ∽ t1 ,..., xn ∽ tn ) R ( x1 ,..., xn ) for some fresh variables x1 ,..., xn , which is permissible. (My notation is slightly different from the book’s, and follows English word order better.)
Partial designation of terms is now handled very simply by making the interpretation and evaluation of terms a partial function. This gives a Meinongian view of designation (“being”), which is distinct from existence.
A final chapter deals with definite descriptions, using Russell’s ι x . ψ (“the x such that ψ”) notation. However, Russell’s paraphrase, translating away definite descriptions, does not work because of questions related to existence. In the discussion here (Definition 12.7.1 ff.), the roles of &jgr; and ψ are interchanged. (This is the only mistake I spotted in the book.) The tableau rules are a bit complicated, but this is a known problem with definite descriptions. One weakness is that definite descriptions are underutilized: modal operators in the ψ formula are only considered in Exercise 12.4.6.
These are minor quibbles. The book’s achievement is to clearly separate several of the concepts that have been conflated in discussions of modal predicate logic and to formalize them, with illuminating examples and exercises. Here is another example. A virus’s action is described as follows: The virus attaches itself to the cell wall of the bacterium with its tail fibers, punctures the wall, and squirts its DNA into the bacterium. The DNA makes copies of the virus. Abbreviating ( &lgr; x ∽ ι x . ψ ) &jgr; by ( &lgr; ! x : ψ ) &jgr; , we can describe this by
Virus ( v ) ∧ Bacterium ( b ) ∧ ( &lgr; ! t : Tailof ( t, v ) , ! w : Wallof ( w, b ) )
Attach ( t, w ) ∧ ⋄ &jgr;1 , &jgr;1 ≡ Punctured ( w ) →
( &lgr; ! d : DNAof ( d, b ) ) Squirt ( d, b ) ∧ ⋄&jgr;2 ,
&jgr;2 ≡ ( ∀ v′ ) Make ( d, v′ ) → Virus ( v′ ) ∧ Copy ( v, v′ ).
The &lgr; abstraction for predicates was used by Fitting as early as 1972 [1], while the need for a scope distinction was argued by Mendelsohn in the context of free logic [2]. This book brings together logic and philosophy in a coherent framework. The treatment is strikingly simple when compared to earlier work by Bressan [3] and Gallin [4]. There is now an extension of this approach to higher-order modal logics [5].
This book will of course be of interest to the logic in computer science community. The &lgr; notation is a very restricted quantifier. When added to propositional modal logic, it does not disturb decidability. The authors even give an example of how the assignment operation can be modeled if one works with propositional dynamic logic (Section 10.3). I would also recommend the book to researchers in artificial intelligence interested in a logical approach to knowledge and natural language representation.
