A Simple Token Game and its Logic
Christian G. Fermüller, Robert Freiman, Timo Lang · EPiC series in computing · 2024
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.