Hybrid Logic

Origin. Arthur Prior introduced nominals for temporal logic (1967). Modern hybrid logic developed by Patrick Blackburn and colleagues (1990s-2000s). Extends modal logic with explicit reference to worlds/states. Bridges modal and first-order logic while maintaining modal decidability. Useful for temporal databases, spatial reasoning, and description logics.

Models. Modal logic with names for worlds. Standard modal logic quantifies over accessible worlds implicitly (□φ = "in all accessible worlds, φ"). Hybrid logic adds nominals (names for specific worlds) and satisfaction operators (@ᵢφ = "at world i, φ holds"). Can express properties modal logic cannot: "there exists a world where φ" without requiring accessibility.

Formalism.

Syntax: Modal logic extended with:

Nominals: i, j, k, ... — atomic formulas true at exactly one world
Satisfaction operator: @ᵢφ — φ is true at the world named i
Downarrow binder (optional): ↓x.φ — bind current world to x, then evaluate φ

Basic hybrid language:

Formulas: p | i | ¬φ | φ ∧ ψ | ◇φ | @ᵢφ
Nominals are both terms (naming worlds) and formulas (true at their world)

Semantics: Kripke model M = (W, R, V, g) where:

W: worlds
R: accessibility
V: valuation (V(i) is a singleton for nominals)
g: assignment of nominals to worlds

Truth:

M, w ⊨ i iff w = g(i)
M, w ⊨ @ᵢφ iff M, g(i) ⊨ φ
M, w ⊨ ↓x.φ iff M, w ⊨ φ[x := w]

Expressive power:

@ᵢp: "p holds at world i" (localized assertion)
@ᵢ◇j: "j is accessible from i" (accessibility as formula)
@ᵢ◇j → @ⱼ◇i: "if j accessible from i, then i from j" (symmetry, expressible!)
◇i: "current world can reach i" (named accessibility)

Comparison with modal logic: Modal logic cannot express "R is irreflexive" (no world accesses itself). Hybrid logic: ↓x.¬◇x — bind the current world to x, then deny that it reaches itself.

Named models: Hybrid logic can internalize frame conditions. @ᵢ◇i expresses reflexivity at i.

Symbols.

Symbol	Unicode	Name	Meaning
i, j, k	—	Nominals	World names
@ᵢ	—	Satisfaction operator	"At world i"
↓	U+2193	Downarrow	Bind current world
□	U+25A1	Box	All accessible worlds
◇	U+25C7	Diamond	Some accessible world
E	—	Existential modality	Some world (global)
A	—	Universal modality	All worlds (global)
∃	U+2203	Quantifier (over nominals)	For some world name
∀	U+2200	Quantifier (over nominals)	For all world names

Metatheory. Basic hybrid logic H(@) is decidable and PSPACE-complete (Areces, Blackburn, and Marx 1999) — no harder than K, so nominals and @ are free. Adding the global modality E raises satisfiability to EXPTIME-complete. Adding ↓ gives the expressiveness of the bounded fragment of first-order logic and makes satisfiability undecidable, though restricted fragments recover decidability. Completeness: pure axioms (containing nominals but no propositional variables) axiomatize the frame classes they define automatically — a general completeness theorem with no modal analogue. Interpolation and Beth definability hold, repairing a failure of many modal logics.

Applies to. Temporal databases (named time points). Spatial reasoning (named locations). Description logics (ABox assertions as hybrid formulas). Feature logic in linguistics. Ontology languages. Any modal domain where explicit reference to states matters.

Limitations. More complex than basic modal logic. The binder ↓ can encode undecidable problems if unrestricted. Nominals inflate the language — each named state needs a symbol. Less widely implemented than pure modal logics. Some elegance of modal abstraction is lost by explicit naming.