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: ¬◇i where i names current world (using ↓i).

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 is decidable (EXPTIME-complete). Adding ↓ gives full first-order expressiveness over frames but is still decidable for many fragments. Completeness: hybrid logic has well-behaved proof theory; pure axioms (involving only nominals) axiomatize frame classes more directly than modal logic. Interpolation and Beth definability hold. Hybrid logic is "well-behaved" despite increased expressiveness.

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.