Hybrid logics: Characterization, interpolation and complexity

Carlos Areces*, Patrick Blackburn, Maarten Marx

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review


Hybrid languages are expansions of prepositional modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work (for example [BS98, BT98a, BT99]) has focussed on a more constrained system called ℋ(↓,commercial at). We show in detail that ℋ(↓, commercial at) is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations (via a restricted notion of Ehrenfeucht-Fraïssé game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result to emerge is that ℋ(↓, commercial at) corresponds to the fragment of first-order logic which is invariant for generated submodels. We then show that ℋ (↓, commercial at) enjoys (strong) interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage ℋ(commercial at). Finally, we provide complexity results for ℋ(commercial at) and other fragments and variants, and sharpen known undecidability results for ℋ(↓, commercial at).

Original languageEnglish
JournalJournal of Symbolic Logic
Issue number3
Pages (from-to)977-1010
Number of pages34
Publication statusPublished - Sep 2001
Externally publishedYes

Cite this