From semantic games to analytic calculi

Abstract

Games offer a natural and fruitful approach to logic, bridging the traditional semantic and proof-theoretic approach to logic. The present thesis aims to illustrate this connection by investigating a technique of lifting semantic games to provability games and further to analytic calculi. The simplest example of this technique is lifting Hintikka’s game for classical propositional logic to a version of Gentzen’s sequent system LK. We apply this technique to modal logic. To overcome some conceptual issues, we must turn to hybrid logic – an extension of modal logic. The language allows us to refer to worlds within the object language explicitly. In our second case study, we develop a semantic game for choice logic – a framework for jointly dealing with truth and preferences. This game has a richer domain of payoff values, which is inherited by the provability game and the resulting calculus, giving a degree-based notion of validity in the induced logic. Using these ideas, we develop a lifting framework to conduct the lifting for general semantic games. This framework encompasses all known cases in the literature and in this thesis.