Hybrid logic is the bounded fragment of first order logic

Hybrid languages are extended 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, BT99]) has focussed on a more constrained system called H(↓,@). The purpose of the present paper is to show in detail thatH(↓,@) is a modally natural system. We study its expressivity, and provide both model theoretic characterizations (via a restricted notion of Ehrenfeucht-Fräıssé game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result is that H(↓,@) corresponds precisely to the first-order fragment which is invariant for generated submodels