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.

Metatheory. Basic hybrid logic H(@) is decidable and PSPACE-complete (Areces, Blackburn, and Marx 1999) — no harder than K, so nominals and @ add no complexity. 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 over proposition letters holds, with nominals permitted in the interpolant (Areces, Blackburn, and Marx 2001); interpolation over nominals fails for H(@) and is restored by adding ↓ (ten Cate 2005).

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. The gains stop abruptly at ↓. Unrestricted, the binder makes satisfiability undecidable over arbitrary frames and loses the finite model property, and decidability returns only for syntactically restricted fragments rather than by any general repair. The free additions are not free everywhere either: the global modality E raises satisfiability from PSPACE to EXPTIME-complete. Structurally, nominals are not closed under uniform substitution, so hybrid logics are not normal modal logics and the Sahlqvist and canonicity apparatus does not transfer unmodified. Ordinary bisimulation no longer preserves truth, and @ᵢ refers outside the generated submodel, so the generated-submodel and tree-model properties fail and with them the arguments that rest on them. The pure-axiom completeness theorem covers exactly the pure-definable frame classes; for impure hybrid axioms it gives nothing.

© 2026 Lingenic LLC