
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.