Hybrid Logic

1. Motivations for hybrid logic

In the standard Kripke semantics for modal logic, truth is relative to points in a set. Thus, a propositional symbol might have different truth-values relative to different points. Usually, these points are taken to represent possible worlds, times, space, knowledge, states in a computer, or something else. This allows us to formalize natural language statements whose truth-values are relative to for example times, like the statement

it is raining

which has clearly different truth-values at different times. Now, certain natural language statements are true at exactly one time, possible world, or something else. An example is the statement

it is five o'clock 15 March 2006

which is true at the time five o'clock 15 March 2006, but false at all other times. The first kind of natural language statements can be formalized in ordinary modal logic, but the second kind cannot.
A major motivation for hybrid logic is to add further expressive power to ordinary modal logic with the aim of being able to formalize the second kind of statements. This is obtained by adding to ordinary modal logic a second sort of propositional symbols called nominals such that in the Kripke semantics each nominal is true relative to exactly one point. A natural language statement of the second kind (like the example statement with the time five o'clock 15 March 2006) is then formalized using a nominal, not an ordinary propositional symbol (which would be used to formalize the example statement with rainy weather). The fact that a nominal is true relative to exactly one point implies that a nominal can be considered a term referring to a point, for example, if a is a nominal that stands for “it is five o'clock 15 March 2006”, then the nominal a can be considered a term referring to the time five o'clock 15 March 2006. Thus, in hybrid logic a term is a specific sort of propositional symbol whereas in first-order logic it is an argument to a predicate.
Most hybrid logics involve further additional machinery than nominals. There is a number of options for adding further machinery; here we shall consider so-called satisfaction operators. The motivation for adding satisfaction operators is to be able to formalize a statement being true at a particular time, possible world, or something else. For example, we want to be able to formalize that the statement “it is raining” is true at the time five o'clock 15 March 2006, that is, that

at five o'clock 15 March 2006, it is raining.

This is formalized by the formula a:p where the nominal a stands for “it is five o'clock 15 March 2006” as above and where p is an ordinary propositional symbol that stands for “it is raining”. It is the part a: of the formula a:p that is called a satisfaction operator. In general, if a is a nominal and φ is an arbitrary formula, then a new formula a:φ called a satisfaction statement can be built (sometimes the notation @_a is used instead of a:). The satisfaction statement a:φ expresses that the formula φ is true relative to one particular point, namely the point to which the nominal a refers.
To sum up, we have now added further expressive power to ordinary modal logic in the form of nominals and satisfaction operators. Informally, the nominal a has the truth-condition

a is true relative to a point w
    if and only if
the reference of a is identical to w

and the satisfaction statement a:φ has the truth-condition

a:φ is true relative to a point w
    if and only if
φ is true relative to the reference of a

Note that actually the point w does not matter in the truth-condition for a:φ since the satisfaction operator a: moves the point of evaluation to the reference of a whatever the identity ofw.
It is remarkable that nominals together with satisfaction operators allow us to express that two points are identical: If the nominals a and b refer to the points w and v, then the formulaa:b expresses that w and v are identical. The following line of reasoning shows why.

a:b is true relative to a point w
    if and only if b is true relative to the reference of a
    if and only if b is true relative to w
    if and only if the reference of b is identical to w
    if and only if v is identical to w

The identity relation on a set has the well-known properties reflexivity, symmetry, and transitivity, which is reflected in the fact that the formulas

a:a
a:b → b:a
(a:b & b:c) → a:c

are valid formulas of hybrid logic. Also the formula

(a:b & a:φ) → b:φ

is valid. This is the rule of replacement.
Beside nominals and satisfaction operators, in what follows we shall consider the so-called binders ∀ and ↓ allowing us to build formulas ∀aφ and ↓aφ. The binders bind nominals to points in two different ways: The ∀ binder quantifies over points analogous to the standard first-order universal quantifier, that is, ∀aφ is true relative to w if and only if whatever point the nominal a refers to, it is the case that φ is true relative to w. The ↓ binder binds a nominal to the point of evaluation, that is, ↓aφ is true relative to w if and only if φ is true relative to w when a refers to w. It turns out that the ↓ binder is definable in terms of ∀ (as shown below).

2. Formal semantics

The language we consider is the language of ordinary modal logic built over ordinary propositional symbols p, q, r, … as well as nominals a, b, c, … and extended with satisfaction operators and binders. We take the propositional connectives & and ¬ to be primitive; other propositional connectives are defined as usual. Similarly, we take the modal operator □ to be primitive and define the modal operator ◊ as ¬□¬. As the name suggests, binders bind nominals and the notions of free and bound occurrences of nominals are defined analogously to first-order logic. Satisfaction operators do not bind nominals, that is, the free nominal occurrences in a formula a:φ are the free nominal occurrences in φ together with the occurrence of a. We let φ[c/a] be the formula φ where the nominal c has been substituted for all free occurrences of the nominal a. If the nominal a occurs free in φ within the scope of ∀c or ↓c, then the bound nominal c in φ is renamed as appropriate.
We now define models and frames. A model for hybrid logic is a triple (W, R, V) where W is a non-empty set, R is a binary relation on W, and V is a function that to each pair consisting of an element of W and an ordinary propositional symbol assigns an element of the set {0,1}. The pair (W, R) is called a frame. Thus, models and frames are the same as in ordinary modal logic. The elements of W are called worlds and the relation R is called the accessibility relation. The model (W, R, V) is said to be based on the frame (W, R).
An assignment for a model M = (W, R, V) is a function g that to each nominal assigns an element of W. An assignment g′ is an a-variant of g if g′ agrees with g on all nominals save possibly a. The relation M, g, w ⊨ φ is defined by induction, where g is an assignment, w is an element of W, and φ is a formula.

M, g, w ⊨ p iff V(w, p)=1
M, g, w ⊨ a iff w = g(a)
M, g, w ⊨ φ & ψ iff M, g, w ⊨ φ and M, g, w ⊨ ψ
M, g, w ⊨ ¬φ iff not M, g, w ⊨ φ
M, g, w ⊨ □φ iff for any element v of W such that wRv, it is the case that M, g, w ⊨ φ
M, g, w ⊨ a:φ iff M, g, g(a) ⊨ φ
M, g, w ⊨ ∀aφ iff for any a-variant g′ of g, it is the case that M, g′, w ⊨ φ
M, g, w ⊨ ↓aφ iff M, g′, w ⊨ φ where g′ is the a-variant of g such that g′(a) = w.

A formula φ is said to be true at w if M, g, w ⊨ φ; otherwise it is said to be false at w. By convention M, g ⊨ φ means M, g, w ⊨ φ for every element w of W and M ⊨ φ means M, g⊨ φ for every assignment g. A formula φ is valid in a frame if and only if M ⊨ φ for any model M that is based on the frame in question. A formula φ is valid in a class of frames F if and only if φ is valid in any frame in F. A formula φ is valid if and only if φ is valid in the class of all frames. The definition of satisfiability is left to the reader.
Note that the binder ↓ is definable in terms of ∀ as the formula ↓aφ ↔ ∀a(a → φ) is valid in any frame.
The fact that hybridizing ordinary modal logic actually does give more expressive power can for example be seen by considering the formula ↓c□¬c. It is straightforward to check that this formula is valid in a frame if and only if the frame is irreflexive. Thus, irreflexivity can be expressed by a hybrid-logical formula, but it is well known that it cannot be expressed by any formula of ordinary modal logic. Irreflexivity can actually be expressed just by adding nominals to ordinary modal logic, namely by the formula c→□¬c. Other examples of properties expressible in hybrid logic, but not in ordinary modal logic, are asymmetry (expressed by c→□¬◊c), antisymmetry (expressed by c→□(◊c→c)), and universality (expressed by ◊c).

3. Translations

Hybrid logic can be translated into first-order logic with equality, and (a fragment of) first-order logic with equality can be translated back into (a fragment of) hybrid logic. The first-order language under consideration has a 1-place predicate symbol p* corresponding to each ordinary propositional symbol p of modal logic, a 2-place predicate symbol R, and a 2-place predicate symbol =. Of course, the predicate symbol p* will be interpreted such that it relativises the interpretation of the corresponding modal propositional symbol p to worlds, the predicate symbol R will be interpreted using the accessibility relation, and the predicate symbol = will be interpreted using the identity relation on worlds. We let a, b, c, … range over first-order variables. The language does not have constant or function symbols. We shall identify first-order variables with nominals of hybrid logic.
We first translate hybrid logic into first-order logic with equality. Given two new first-order variables a and b, the translations ST_a and ST_b are defined by mutual recursion. We just give the translation ST_a.

ST_a(p) = p*(a)
ST_a(c) = a=c
ST_a(φ & ψ) = ST_a(φ) & ST_a(ψ)
ST_a(¬φ) = ¬ST_a(φ)
ST_a(□φ) = ∀b(R(a, b) → ST_b(φ))
ST_a(c:φ) = ST_a(φ)[c/a]
ST_a(↓cφ) = ST_a(φ)[a/c]
ST_a(∀cφ) = ∀cST_a(φ)

The definition of ST_b is obtained by exchanging a and b. The translation is an extension of the well-known standard translation from modal logic into first-order logic. As an example, we demonstrate step by step how the hybrid-logical formula ↓c□¬c is translated into a first-order formula:

STa(↓c□¬c)	=	STa(□¬c)[a/c]
	=	∀b(R(a, b) → STb(¬c))[a/c]
	=	∀b(R(a, b) → ¬STb(c))[a/c]
	=	∀b(R(a, b) → ¬b=c)[a/c]
	=	∀b(R(a, b) → ¬b=a).

The resulting first-order formula is equivalent to ¬R(a, a) which shows that ↓c□¬c indeed does correspond to the accessibility relation being irreflexive, cf. above.
First-order logic with equality can be translated back into hybrid logic by the translation HT given below.

HT(p*(a)) = a:p
HT(R(a, c)) = a:◊c
HT(a=c) = a:c
HT(φ & ψ) = HT(φ) & HT(ψ)
HT(¬φ) = ¬HT(φ)
HT(∀aφ) = ∀aHT(φ)

Note that the hybrid-logical binder ∀ is needed. The history of the above mentioned observations goes back to the work of Arthur N. Prior, we shall return to that later.
Similarly, the so-called bounded fragment of first-order logic can be translated into the hybrid logic but here only the binder ↓ is needed, as pointed out in the paper Areces, Blackburn, and Marx (2001). The bounded fragment is the fragment of first-order logic with the property that quantifiers only occur as in the formula ∀c(R(a, c) → φ), where it is required that the variables a and c are different. A translation from the bounded fragment to the hybrid logic without the ∀ binder can be obtained by replacing the last clause in the translation HT above by

HT(∀c(R(a, c) → φ)) = a:□↓cHT(φ).

In Areces, Blackburn, and Marx (2001) a number of independent semantic characterisations of the bounded fragment are given.
The translations given above are truth-preserving. To state this formally, one makes use of the well-known observation that models and assignments for hybrid logic can be considered as models and assignments for first-order logic and vice versa. These truth-preservation results are straightforward to formulate and we leave the details to the reader. Thus, the hybrid logic with the binder ∀ has the same expressive power as first-order logic with equality and the hybrid logic without the binder ∀ (but with the binder ↓) has the same expressive power as the bounded fragment of first-order logic (note that the translation ST_a(φ) of any formula φ without the binder ∀ is in the bounded fragment).

4. Arthur N. Prior and hybrid logic

The history of hybrid logic goes back to Arthur N. Prior's hybrid tense logic, which is a hybridized version of ordinary tense logic. With the aim of investigating this further, we shall give a formal definition of hybrid tense logic: The language of hybrid tense logic is simply the language of hybrid logic defined above except that there are two modal operators, namely G andH, instead of the single modal operator □. The two new modal operators are called tense operators. The semantics of hybrid tense logic is the semantics of hybrid logic, cf. earlier, with the clause for □ replaced by clauses for the tense operators G and H.

M, g, w ⊨ Gφ iff for any element v of W such that wRv, it is the case that M, g, w ⊨ φ
M, g, w ⊨ Hφ iff for any element v of W such that vRw, it is the case that M, g, w ⊨ φ

Thus, there are now two modal operators, namely one that “looks forwards” along the accessibility relation and one that “looks backwards”. In tense logic the elements of the set W are called moments or instants and the relation R is called the earlier-later relation.
Of course, it is straightforward to modify the translations ST_a and HT above such that translations are obtained between hybrid tense logic (including the ∀ binder) and first-order logic with equality. The first-order logic under consideration is what Prior called first-order earlier-later logic. Given the translations, it follows that Prior's first-order earlier-later logic has the same expressive power as hybrid tense logic.
Now, Prior introduced hybrid tense logic in connection with what he called four grades of tense-logical involvement. The motivation for his four grades of tense-logical involvement was philosophical. The four grades were presented in the book Prior (1968), Chapter XI (also Chapter XI in the new edition Prior (2003)). Moreover, see Prior (1967), Chapter V.6 and Appendix B.3-4. For a more general discussion, see the posthumously published book Prior and Fine (1977). The stages progress from what can be regarded as pure first-order earlier-later logic to what can be regarded as pure tense logic; the goal being to be able to consider the tense logic of the fourth stage as encompassing the earlier-later logic of the first stage. In other words, the goal was to be able to translate the first-order logic of the earlier-later relation into tense logic. It was with this goal in mind Prior introduced so-called instant-propositions:

What I shall call the third grade of tense-logical involvement consists in treating the instant-variables a, b, c, etc. as also representing propositions. (Prior 1968, p. 122-123)

In the context of modal logic, Prior called such propositions possible-world-propositions. Of course, this is what we here call nominals. Prior also introduced the binder ∀ and what we here call satisfaction operators (he used the notation T(a, φ) instead of a:φ for satisfaction operators). In fact, Prior's third grade tense logic is identical to the hybrid tense logic as defined above. The ↓ binder was introduced much later. Thus, Prior obtained the expressive power of his first-order earlier-later logic by adding to ordinary tense logic further expressive power in the form of nominals, satisfaction operators, and the binder ∀. So from a technical point of view he clearly reached his goal.
However, from a philosophical point of view it has been debated whether or not the ontological import of his third grade tense logic is the same as the ontological import of the first-order earlier-later logic. For example, the ∀ binder is by some authors considered a direct analogy to the first-order ∀ quantifier, and therefore suspect; see for example the paper Sylvan (1996) in the collection Copeland (1996). Also a number of other papers in this collection are relevant. See Braüner (2002) for a discussion of Prior's fourth grade tense logic. See also Øhrstrøm and Hasle (1993), Øhrstrøm and Hasle (2006), Müller (2007), and Blackburn (2007). Finally, see the discussion of Prior's work in the book Braüner (2011).

5. The development of hybrid logic since Prior

The first completely rigorous definition of hybrid logic was given in Robert Bull's paper Bull (1970) which appeared in a special issue of the journal Theoria in memory of Prior. Bull introduces a third sort of propositional symbols where a propositional symbol is assumed to be true exactly at one branch (“course of events”) in a branching time model. This idea of sorting propositional symbols according to restrictions on their interpretations has later been developed further by a number of authors, see Section 5 of the paper Blackburn and Tzakova  (1999) for a discussion.
The hybrid logical machinery originally invented by Prior in the late 1960s was reinvented in the 1980s by Solomon Passy and Tinko Tinchev from Bulgaria, see Passy and Tinchev (1985) as well as Passy and Tinchev (1991). Rather than ordinary modal logic, this work took place in connection with the much more expressive Propositional Dynamic Logic.
A major contribution in the 1990s was the introduction of the ↓ binder by Valentin Goranko, see the papers Goranko (1994) and Goranko (1996). Since then, hybrid logic with the ↓ binder has been extensively studied by a number of people, notably Patrick Blackburn and his collaborators, see for example the paper Areces, Blackburn, and Marx (2001) on model-theoretic aspects of this logic. A recent very comprehensive study of the model-theory of hybrid logic is the PhD thesis of ten Cate (2004).
Also the weaker hybrid logic obtained by omitting both of the binders ↓ and ∀ has been the subject of extensive exploration. It turns out that this binder-free logic and a number of variants of it are decidable. In the paper Areces, Blackburn, and Marx (1999), a number of complexity results are given for hybrid modal and tense logics over various classes of frames, for example arbitrary, transitive, linear, and branching. It is remarkable that the satisfiability problem of the binder-free hybrid logic over arbitrary frames is decidable in PSPACE, which is the same as the complexity of deciding satisfiability in ordinary modal logic. Thus, hybridizing ordinary modal logic gives more expressive power, but the complexity stays the same. Some work has been carried out on simulating nominals inside modal logic, see Kracht and Wolter (1997).
It is remarkable that first-order hybrid logic offers precisely the features needed to prove interpolation theorems: While interpolation fails in a number of well-known first-order modal logics, their hybridized counterparts have this property, see Areces, Blackburn, and Marx (2003) as well as Blackburn and Marx (2003). The first paper gives a model-theoretic proof of interpolation whereas the second paper gives an algorithm for calculating interpolants based on a tableau system.
It should also be mentioned that logics similar to hybrid logics play a central role within the area of description logic, which is a family of logics used for knowledge representation in Artificial Intelligence, see the paper Blackburn and Tzakova (1998) and Carlos Areces' PhD thesis (2000).

6. Proof methods for hybrid logic

A number of papers have dealt with axioms for hybrid logic, for example Blackburn (1993) and Blackburn and Tzakova (1999). The latter paper gives an axiom system for hybrid logic and shows the remarkable result that if the axiom system is extended with a set of additional axioms which are pure formulas (that is, formulas where all propositional symbols are nominals), then the extended axiom system is complete with respect to the class of frames validating the axioms in question. Pure formulas correspond to first-order conditions on the accessibility relation (cf. the translation ST_a above), so axiom systems for new hybrid logics with first-order conditions on the accessibility relation can be obtained in a uniform way simply by adding axioms as appropriate. So, if for example the formula ↓c□¬c is added as an axiom, then the resulting system is complete with respect to irreflexive frames, cf. earlier. The paper Blackburn and ten Cate (2006) investigates orthodox proof-rules (which are proof-rules without side-conditions) in axiom systems, and it is shown that if one requires extended completeness using pure formulas, then unorthodox proof-rules are indispensable in axiom systems for binder-free hybrid logic, but an axiom system can be given only involving orthodox proof-rules for the stronger hybrid logic including the ↓ binder. See also the paper Braüner (2006) (and the book Braüner (2011)) which gives another axiom system for hybrid logic as well as axiom systems for intuitionistic and paraconsistent hybrid logic.
Tableau, Gentzen, and natural deduction style proof-theory for hybrid logic work very well compared to ordinary modal logic. Usually, when a modal tableau, Gentzen, or natural deduction system is given, it is for one particular modal logic and it has turned out to be problematic to formulate such systems for modal logics in a uniform way without introducing metalinguistic machinery. This can be remedied by hybridization, that is, hybridization of modal logics enables the formulation of uniform tableau, Gentzen, and natural deduction systems for wide classes of logics. The paper Blackburn (2000) introduces a tableau system for hybrid logic that has this desirable feature: Analogous to the axiom system of Blackburn and Tzakova (1999), completeness is preserved if the tableau system is extended with a set of pure axioms, that is, a set of pure formulas that are allowed to be added to a tableau during the tableau construction. The tableau system of Blackburn (2000) is the basis for a decision procedure for the binder-free fragment of hybrid logic given in Bolander and Braüner (2006). This line of work has been continued in the papers Bolander and Blackburn (2007) and Bolander and Blackburn (2009). The paper Cerrito and Cialdea (2010) presents another tableau-based decision procedure for hybrid logic. Other decision procedures for hybrid logics, which also are based on proof-theory, are given in the paper Kaminski and Smolka (2009). The procedures of the latter paper are based on a higher-order formulation of hybrid logic involving the simply typed lambda calculus.
The paper Hansen, Bolander, and Braüner (2008) gives a tableau-based decision procedure for many-valued hybrid logic, that is, hybrid logic where the two-valued classical logic basis has been generalized to a many-valued logic basis involving a truth-value space having the structure of a finite Heyting algebra. Hansen (2010) gives a tableau-based decision procedure for a hybridized version of a dynamic epistemic logic called public annoucement logic. This is also a major issue of the forthcoming PhD thesis Hansen (2011).
Natural deduction style proof-theory of hybrid logic has been explored in the papers Braüner (2004a), Braüner (2004b), Braüner (2005a), and Braüner (2005b). The paper Braüner (2004a) also gives a Gentzen system for hybrid logic. These natural deduction and Gentzen systems can be extended with additional proof-rules corresponding to first-order conditions on the accessibility relations expressed by so-called geometric theories (this is of course analogous to extending tableau and axiom systems with pure axioms). See also Braüner and de Paiva (2006) where a natural deduction system is given for intuitionistic hybrid logic. In the context of situation theory, Gentzen and natural deduction systems for logics similar to hybrid logics were explored already in the early 1990s by Jerry Seligman, see the overview in Seligman (2001). See the book Braüner (2011) for a detailed treatment of hybrid-logical proof-theory.
Work in resolution calculi and model checking is in the early phases, see Areces, de Rijke, and de Nivelle (2001) for resolution calculi and see as Franceschet and de Rijke (2006) as well as Lange (2009) for results on model checking.
Since the mid 1990s, the work on hybrid logic has flourished. For a detailed overview, see the handbook chapter Areces and ten Cate (2006). We refer the reader to the publications in the bibliography for further references. Moreover, see the internet resources below.