Repairing the interpolation theorem in quantified modal logic

Quantified hybrid logic is quantified modal logic extended with apparatus for nam-ing states and asserting that a formula is true at a named state. While interpolation and Beth’s definability theorem fail in a number of well known quantified modal logics (for example in quantified modal K, T, D, S4, S4.3 and S5 with constant domains), their counterparts in quantified hybrid logic have these properties. These are special cases of the main result of the paper: the quantified hybrid logic of any class of frames definable in the bounded fragment of first-order logic has the interpo-lation property, irrespective of whether varying, constant, expanding, or contracting domains are assumed. Key words: quantified modal logic, quantified hybrid logic, interpolation, Beth definability, bounded fragment. 1991 MSC: 03B45, Modal Logic Hybrid logics are extensions of orthodox modal logics in which it is possible to name states (or worlds, or times, or locations...) and to assert that a formula is true at a named state (see for example [10,9,3,8,1], Chapter 7 of [2], and the webpage www.hylo.net). Arguably such extensions are interesting from an applied perspective: we often want to reason about what happens at particular states, worlds, times, or locations, and this isn’t possible in orthodox modal logics. For the purposes of the present paper, however, the important point? Areces is supported by NWO-grant 365-20-005. Marx is supported by NWO