What are Hybrid Logics

"Hybrid Logic" is a loose term covering a number of logical systems living somewhere between modal and classical logic.

In their simplest form, hybrid languages are modal languages which use formulas to refer to specific points in a model. To build a simple hybrid language, take an ordinary language of propositional modal logic (built over some collection of propositional variables p, q, r and so on), and add a second type of atomic formula. These new atoms are called nominals, and are typically written i, j and k. Both types of atoms can be freely combined to form more complex formulas in the usual way; for example

is a well formed formula.

Now for the key idea: insist that each nominal must be true at exactly one point in any model. Thus a nominal names a point by being true there and nowhere else. This simple idea gives rise to richer logics. Note, for example, that the previous formula is valid: if the antecedent is satisfied at a point m, then the unique point named by i must be accessible from m, and both p and q must be true there. Note that this is the case only because i is a nominal: if we replace i by an ordinary propositional symbol r, then the formula is not valid any more.

Nominals enable us to define classes of frames that ordinary modal languages cannot. Let's see an example. The formula

forces the transition relation to be irreflexive. Quite clearly, this formula says that if i is the name of the current point (the point at which we are evaluating) then that point should not be reachable by the accessibility relation. That is, no point should be able to access itself. The only way to guarantee this is if the accessibility relation is irreflexive, so this formula is valid on precisely those frames with this property (that is, it defines the irreflexive frames). Compare this formula with its modal analog . Notice that the possibility that p is true at more that one point transforms the meaning completely: asks for an arbitrary p-point in the model to be unreachable if p is true. In fact, not only does not define irreflexivity, it is well known that no formula whatsoever in the classical modal language of diamonds and boxes can do so. So nominals really do enhance the expressive power of the language.

Once we have nominals, another interesting idea immediately suggests itself: why not allow ourselves to specify what is going on at points named by nominals? That is, why not introduce an operator that allows us to jump to the point named by a nominal, and see if some formula is true there? This is exactly what the formula does: it moves the point of evaluation to the point named by i and checks whether is true there.

Now, may well be familiar to you if you work in logic or Artificial Intelligence (AI). For a start, is just Prior's construct (" is true at time i"), which he used to define his "third grade tense logics" [Prior 1967]. Third grade tense logic, incidentally, was Prior's term for what we call hybrid languages. It is also the Holds operator introduced in [Allen 1984] for temporal representation in AI. Finally, the same operator is used in the "Topological Logic" of [Rescher and Urquhart 1971].

The operator has many nice logical properties. For a start, it is a normal modal operator as it satisfies distributivity over and the Generalization Rule. It is also self dual: is valid. But most importantly, it works as a bridge between semantics and syntax. The intuition here is the following connection

where i is a nominal naming w. In other words, allows the satisfaction relation itself to be talked about in the object language. For this reason, is often called the satisfaction operator.

Once we have realized the potential provided by direct reference to specific points in the model, the way lies open for further enrichments. The most obvious is to regard nominals not as names but as variables over individual points, and to add quantifiers. That is, we now allow expressions like

to be formed. This sentence is satisfied at a point m if and only if from every point x that is accessible from m we can reach at least one reflexive point y. No formula with this property exists in ordinary modal languages, or even in modal languages enriched with nominals.

The binder (and its dual ) has been introduced on several occasions, for quite distinct purposes. The earliest treatments are probably those of [Prior 1967], [Prior 1968] Chapter V.6, and [Bull 1970]. About fifteen years later (and independently of Prior and Bull) Passy and Tinchev hybridised Propositional Dynamic Logic with the help of . They remark that the idea of was suggested to them by Skordev (who in turn was inspired by certain investigations in recursion theory). An excellent overview of this line of work and its connections with other branches of extended modal logic can be found in [Passy and Tinchev 1991].

The idea of binding variables to points underlies much current work on hybrid languages, but for many purposes the binder is arguably too strong: languages which employ obscure the locality intuition central to Kripke semantics. To evaluate a modal formula we need to specify some point m (the current point) and begin evaluation there. The function of the modalities is to scan the points accessible from m, the points accessible from those points, and so on; in short, m is the starting point for step-wise local exploration of the model. Languages which allow variables to be bound to arbitrary points don't mesh well with this intuition.

For this reason, recent work on binding nominals has focussed on hybrid languages with a different kind of binder. The binder binds variables to points, but, unlike , it does so in an intrinsically local way: it binds variables to the current point. In essence it enables us to create a name for the here-and-now. For example, using we would write

for irreflexivity. Again, the intuitive reading is quite straightforward: the formula says "call the actual point x and ensure that x is not reachable."

Like , the binder has been independently invented on a number of occasions. For example, [Richards, Bethke, van der Does, and Oberlander 1989] introduce as part of an investigation into temporal semantics and temporal databases (it's their G operator), [Sellink 1994] uses it to aid reasoning about automata, and [Cresswell 1990] uses it as part of his treatment of indexicality. Nonetheless, none of the systems just mentioned allows the free syntactic interplay of variables with the underlying propositional logic; that is, they make use of , but in languages that aren't fully hybrid. The earliest paper to introduce into a fully hybrid language seems to be [Goranko 1994].

Note that the operator is a natural counterpart to . Whereas "stores" the current point (by binding a variable to it), enables us to "retrieve" points. A number of recent papers deal with languages containing the operator. [Blackburn and Seligman 1998] relates it to other hybrid languages, [Blackburn and Tzakova 1999] studies it axiomatically and [Blackburn 1998,Tzakova 1999] develop analytic proof techniques for them. In [Areces, Blackburn, and Marx 1998] the model theoretic properties of the language are analyzed, and the fragment of first-order logic it corresponds to is characterized both syntactically and semantically.