Constructive interpolation in hybrid logic

Patrick Blackburn, Maarten Marx

Research output: Contribution to journalJournal articlepeer-review


Craig’s interpolation lemma (if φ → ψ is valid, then φ → θ and θ → ψ are valid, for � a formula constructed using only primitive symbolswhich occur both inφ and φ → ψ) fails for many propositional and �rst order modal logics. The interpolation property is often regarded as a sign of well-matched syntax and semantics. Hybrid logicians claim that modal logic is missing important syntactic machinery, namely tools for referring to worlds, and that adding such machinery solves many technical problems. The paper presents strong evidence for this claim by de�ning interpolation algorithms for both propositional and �rst order hybrid logic. These algorithms produce interpolants for the hybrid logic of every elementary class of frames satisfying the property that a frame is in the class if and only if all its point-generated subframes are in the class. In addition, on the class of all frames, the basic algorithm is conservative: on purely modal input it computes interpolants in which the hybrid syntactic machinery does not occur.

Original languageEnglish
JournalJournal of Symbolic Logic
Issue number2
Pages (from-to)463-480
Number of pages18
Publication statusPublished - Jun 2003
Externally publishedYes

Cite this