This chapter is designed to outline some techniques, results, and new trends in quantified modal logics. Since it is directed to readers not specialized in the field of modal logic, we will start “from the beginning” and so discuss some basic material; at the same time, we intend to offer an idea of some of the recent research in the area and of possible directions for future research.

Quantified modal logics contain – in addition to classical connectives and quantifiers – a unary operator, the “box” operator □, whose meaning can be variously interpreted depending on the context and on the applications. Here is a list of possible readings of □A (taken from [15]):

1. It is necessarily true that A;

2. It will always be true that A;

3. It ought to be that A;

4. It is known that A;

5. It is believed that A;

6. It is provable in Peano arithmetic that A;

7. After the program terminates, A.

A natural semantic demand is that the truth value of a sentence such as □A be determined (according to some of the above readings) once the truth value of A is known in a suitable set of “instants of time” or “states of affairs” that are considered as alternative to the actual one. Consequently, a semantics for quantified modal logic should contain a mathematical formalization of the following entities: (a) the different “worlds”; (b) the relation of “being conceivable as an alternative”; and (c) the objects or individuals “existing” in them and the connections between these.