Hybrid logic

Go to home page

Hybrid formulas and elementarily generated modal logics

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.

Axiomatizing hybrid logic using modal logic

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.

A bisimulation characterization theorem for hybrid logic with the current-state binder

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.

Bounded fragment and hybrid logic with polyadic modalities

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.