Hybrid logic
Go to home page
Ian Hodkinson
Notre Dame J. Formal Logic 47 (2006) 443-478.
We show that the modal logics of elementary classes of Kripke frames
are precisely those logics that can be captured by sets of
pure positive hybrid sentences with arbitrary existential and
relativised universal quantification over nominals. Each such
hybrid sentence generates an infinite set of modal formulas called
'approximants', which together axiomatise a canonical modal logic that
is sound and complete for the class of frames validating the
hybrid sentence. This generalises to sets of hybrid sentences.
The proof is analogous to standard proofs of Sahlqvist's theorem.
Ian Hodkinson and Louis Paternault
Journal of Applied Logic 8 (2010) 386-396, doi:10.1016/j.jal.2010.08.005.
We study hybrid logics with nominals and 'actuality' operators @.
We recall the method of ten Cate, Marx, and Viana to simulate hybrid logic using modalities and 'nice'
frames, and we show that the hybrid logic of a class of frames is the modal logic of the class of its corresponding nice frames.
Using these results, we show how to axiomatize the hybrid logic of any elementary class of frames.
Then we study quasimodal logics, which are hybrid logics axiomatized by modal axioms together with basic
hybrid axioms common to any hybrid logic, using only orthodox inference rules. We show that the hybrid
logic of any elementary modally definable class of frames, or of any elementary class of frames closed under
disjoint unions, bounded morphic images, ultraproducts and generated subframes, is quasimodal. We also
show that the hybrid analogues of modal logics studied by McKinsey--Lemmon and Hughes are quasimodal.
Ian Hodkinson and Hicham Tahiri
Review of Symbolic Logic 3 (2010) 247-261.
doi:10.1017/S1755020309990426, published online by Cambridge University Press 26 Feb 2010.
Copyright Cambridge University Press
We prove that every first-order formula that is invariant under quasi-injective
bisimulations is equivalent to a formula of hybrid logic
with the downarrow operator. Our proof uses a
variation of the usual unravelling technique. We also briefly survey related results, and show in a standard way that it is undecidable whether a first-order formula is invariant under quasi-injective bisimulations.
Ian Hodkinson
Review of Symbolic Logic 3 (2010) 279-286
doi:10.1017/S1755020309990402, published online by Cambridge University Press 22 Mar 2010.
Copyright Cambridge University Press
We show that the bounded fragment of first order logic and the hybrid language
with 'downarrow' and 'at' operators are equally expressive even with polyadic modalities,
but that their 'positive' fragments are equally expressive only
for unary modalities.
Ian Hodkinson
Submitted, 2024
We prove a van Benthem-Rosen-style characterisation theorem for two basic hybrid logics: modal logic with nominals, and modal logic with nominals and @. In each case, we show that over all Kripke models, and over all finite Kripke models, every first-order formula that is invariant under the appropriate bisimulations is equivalent to a hybrid formula, and we give optimal bounds on its modal depth in terms of the quantifier depth of the first-order formula.
We also show by example that the characterisation for modal logic with nominals does not extend to arbitrary bisimulation-closed classes of Kripke models.