# 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.