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.

We introduce a simple game of resource-conscious reasoning. In this two-player game, players P and O place tokens of positive and negative polarity onto a game board according to certain rules. P wins if she manages to match every negative token with a corresponding positive token. We study this token game using methods from computational complexity and proof theory. Specifically, we show complexity results for various fragments of the game, in- cluding PSPACE-completeness of a finite restriction and undecidability of the full game featuring non-terminating plays. Moreover, we show that the finitary version of the game is axiomatisable and can be embedded into exponential-free linear logic. The full game is shown to satisfy the exponential rules of linear logic, but is not fully captured by it. Finally, we show determinacy of the game, that is the existence of a winning strategy for one of the players.

Group polarization, the phenomenon where individuals become more extreme after in- teracting, has been gaining attention, especially with the rise of social media shaping peo- ple’s opinions. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this work we consider the modal logic PNL that captures the no- tion of agents agreeing or disagreeing on a given topic. Our contribution involves enhancing PNL with advanced formal reasoning techniques, instead of relying on axiomatic systems for analyzing group polarization. To achieve this, we introduce a semantic game tailored for (hybrid) extensions of PNL. This game fosters dynamic reasoning about concrete net- work models, aligning with our goal of strengthening PNL’s effectiveness in studying group polarization. We show how this semantic game leads to a provability game by systemically exploring the truth in all models. This leads to the first cut-free sequent systems for some variants of PNL. Using polarization of formulas, the proposed calculi can be modularly adapted to consider different frame properties of the underlying model.