Kluwer Academic Pub., Norwell, MA, 1999, 287 pp., ISBN 0-7923-5334-X

**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(t_{1},...,t_{n}) is not allowed.
But this is easy to rectify: translate it to
(*lambda* x_{1}:t_{1},...,x_{n}:t_{n})
R(x_{1},...,x_{n})
for some fresh variables x_{1},...,x_{n},
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 P _{1} and Diamond P_{2},
*

P_{1} = Punctured(w) implies (lambda !d: DNA_of(d,v)) Squirt(d,b),

P_{2} = (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.