ACM CR Categories: F.4.1 Mathematical logic - Modal logic (P), I.2.4 Knowledge representation formalisms and methods - Modal logic
Modal logic is widely used in computer science ever since it was seen that Kripke's possible world semantics can model transition systems, which our subject abounds in. 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. See the variety of semantics possible in Garson and Cochiarella's chapters in [H].
Fitting and Mendelsohn give a clean treatment of first-order modal logic in this monograph. After three chapters on propositional modal logics providing the setting, they show in the next five chapters 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. But the focus of the book is on actualist quantifiers, which have proved more thorny 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 (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 Diamond P(t), is the term t to be evaluated in the current world or in the one whose possibility is being talked of? Thus, 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 Diamond (lambda x : pm) Twd(x) and (lambda x : pm) Diamond Twd(x) (Diamond referring to the time of independence, and Twd 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 (lambda 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. Fitting and Mendelsohn would use Diamond <lambda x.Twd(x)>(pm) and <lambda x.Diamond Twd(x)>(pm) emphasizing that the lambda-abstraction is a predicate-forming operation, analogous to Schönfinkel's function-forming notation. The notation used here 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 iota x. P (``the x such that P'') 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 rôle of phi and psi is 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 a bit under-utilized: modal operators in the P formula are only considered in Exercise 12.4.6.
But these are minor quibbles. The achievement of the book is to clearly separate several of the concepts that have been conflated together 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 fibres, punctures the wall, and squirts its DNA into the bacterium. The DNA makes copies of the virus. Abbreviating (lambda x: iota x. P) Q by (lambda !x: P) Q, we can describe this by:
Virus(v) and Bacterium(b) and
(lambda !t: Tail_of(t,v), !w: Wall_of(w,b))
Attach(t,w) and Diamond P1 and Diamond P2,
P1 = Punctured(w) implies
(lambda !d: DNA_of(d,v)) Squirt(d,b),
P2 = (for all v') Make(d,v') implies Virus(v') and Copy(v,v').
The lambda abstraction for predicates was used by Fitting as early as [F], while the need for a scope distinction was argued by Mendelsohn [M] in the context of free logic. This book brings together logic and philosophy in a coherent framework. The treatment is strikingly simple when compared to earlier work by Bressan [B] and Gallin [G]. There is now an extension of this approach to higher-order modal logics [T].
This book will of course be of interest to the ``logic in computer science'' community. The lambda notation is a very restricted kind of quantifier. When added to propositional modal logic, it does not disturb decidability. There is even an example of how the assignment operation can be modelled 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.
References
[B] A. Bressan, A general interpreted modal calculus. Yale University Press, 1973.
[F] M.C. Fitting, An epsilon-calculus system for first-order S4. In W. Hodges (ed.), Conference in Mathematical Logic, London '70, LNM 255, Springer, 1972, pp. 103-110.
[G] D. Gallin, Intensional and higher-order modal logic. North Holland, 1975.
[H] D. Gabbay and F. Guenthner (eds.), Handbook of philosophical logic, Kluwer, 1984.
[M] R.L. Mendelsohn, Objects and existence: reflections on free logic. Notre Dame J. Formal Logic Vol. 30, No. 4 (Fall 1989), pp. 604-623.
[T] M.C. Fitting, Types, tableaus, and Gödel's god, Kluwer, 2002.