Hybrid logics: Characterization, interpolation and complexity

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).