Hybrid logics: characterization, interpolation and complexity

C. Areces, P. Blackburn, and M. Marx. Hybrid logics: characterization, interpolation and complexity. The Journal of Symbolic Logic, 66(3):977–1010, 2001.

Download

[pdf] 

Abstract

Hybrid languages are expansions of propositional 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 H(\downarrow, @). We show in detail that H(\downarrow, @) is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations (via a restricted notion of Ehrenfeucht- Fraisse game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result to emerge is that H(\downarrow, @) corresponds to the fragment of first-order logic which is invariant for generated submodels. We then show that H(\downarrow, @) enjoys (strong) interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage H(@). Finally, we provide complexity results for H(@) and other fragments and variants, and sharpen known undecidability results for H(\downarrow, @).

BibTeX

@Article{Areces2001f,
  author =       "C. Areces and P. Blackburn and M. Marx",
  journal =      "The Journal of Symbolic Logic",
  title =        "Hybrid logics: characterization, interpolation and
                 complexity",
  year =         "2001",
  number =       "3",
  abstract =     "Hybrid languages are expansions of propositional 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 H(\downarrow, @). We show in detail that
                 H(\downarrow, @) is modally natural. We begin by
                 studying its expressivity, and provide model theoretic
                 characterizations (via a restricted notion of
                 Ehrenfeucht- Fraisse game, and an enriched notion of
                 bisimulation) and a syntactic characterization (in
                 terms of bounded formulas). The key result to emerge is
                 that H(\downarrow, @) corresponds to the fragment of
                 first-order logic which is invariant for generated
                 submodels. We then show that H(\downarrow, @) enjoys
                 (strong) interpolation, provide counterexamples for its
                 finite variable fragments, and show that weak
                 interpolation holds for the sublanguage H(@). Finally,
                 we provide complexity results for H(@) and other
                 fragments and variants, and sharpen known
                 undecidability results for H(\downarrow, @).",
  pages =        "977--1010",
  volume =       "66",
}