Games for Hybrid Logic -- From Semantic Games to Analytic Calculi

TL;DR

This paper explores how game semantics for hybrid logic can be transformed into a proof system by finitizing the search for winning strategies, bridging semantics and proof theory.

Contribution

It introduces a method to convert the search for winning strategies in hybrid logic into a finitized, systematic proof system.

Findings

Winning strategies can be finitized and systematically searched.

A formal link between game semantics and proof systems is established.

Hybrid logic's semantics can be effectively represented in proof form.

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. The main result is that the systematic search of winning strategies over all models can be finitized and thus reformulated as a proof system.