Games for hybrid logic from semantic games to analytic calculi

Abstract Game semantics and winning strategies offer a potential conceptual bridge between semantics and proof systems of logics. We illustrate this link for hybrid logic—an extension of modal logic that allows for explicit reference to worlds within the language. We lift a Hintikka-style semantic game to a disjunctive game. The disjunctive game adequately models entailment and validity over classes of frames characterizable in the hybrid language. The search for winning strategies in this game can be reformulated as a sequent-style proof system.