From Semantic Games to Analytic Calculi – and Back

This project lies at the intersection of logic and game theory. A fundamental concern in logic is the relation between the syntactical form of a statement, and the semantic structures (models) in which the statement is evaluated. One might be interested in whether a statement holds in a particular structure i.e. in the (relative) truth of the statement or whether it holds in a whole class of possible structures i.e. in the validity of the statement. Perhaps surprisingly, for both concepts there often exist characterizations in terms of formal two player games: semantic games and provability games, respectively. A crucial notion in both kind of games (and in game theory, generally) is that of a winning strategy a strategy that we can follow so that we win against any opponent, no matter which moves he or she makes. Given a statement and a structure, in semantic games, a winning strategy exists if and only if the statement is true in the structure. In provability games, instead, a winning strategy exists if and only if the statement is valid. Intuitively, one should be able to turn a semantic game into a provability game by abstracting away from the given structure. Indeed, this approach has been successful at least once in the past, for a specific many-value logic (Lukasiewicz logic), yielding even more than expected: the so-constructed provability games led also to the introduction of an analytic calculus, i.e. a well-behaved system for the formal derivation of valid statements. The main aim of this project is to generalize this result and to explore systematic methods for turning semantic games into provability games and further into analytic calculi. Moreover, we also want to go into the other direction and explore routes for interpreting analytic calculi as provability games and, finally, in terms of semantic games. The novelty of our approach lies in a rather wide and unifying view: rather than treating particular positive cases in isolation, we aim to obtain results that apply to whole classes of games and calculi.

This project has been located at the intersection of logic and game theory. A fundamental concern of logic is the relationship between the syntactic form of a statement and the semantic structures (interpretations, models) in which the statement is evaluated. One can be interested in whether a statement holds in a particular structure - i.e. for the (relative) truth of the statement - or whether it holds in a whole class of possible structures - i.e. for the validity of the statement. Interestingly, there are characterizations of both concepts in the form of formal games with two players: semantic games and provability games, respectively. A crucial notion in both types of games (and in game theory in general) is that of a winning strategy - a strategy that we can follow to win against any opponent, no matter what moves he makes. In semantic games, given a statement and a structure, there is a winning strategy if only if the statement is true in the given structure In provability games, on the other hand, a winning strategy signifies that the statement is valid. Intuitively, one should be able to turn a semantic game into a provability game by abstracting from the given structure. In fact, this approach has been successful at least once in the past, for a certain many-valued logic (Lukasiewicz logic), where even more came out than expected: The proof games constructed in this way also led to the introduction of an analytic calculus, i.e. a well-functioning system for the formal derivation of valid statements. The main goal of this project was to generalize this result and to explore systematic methods to transform semantic games into provability games and further into analytic proof systems. To achieve this goal, we applied the outlined methodology to different types of logic. In this way, we were able to transform a truth comparison game for Gödel logic, an important fuzzy logic, into a proof game that can be transformed into an analytic calculus of a special format with comparison pairs of formulas as base objects. A further generalization of this kind concerns hybrid modal logic, which in fact consists of a whole family of logics that allow different propositional states to be explicitly named and referred to. We also successfully applied our game based approach to logics for reasoning about group polarization in social networks, yielding corresponding semantic games, provability games, as well as analytic calculi. Most importantly, we have adapted and refined the methodology to provide a general framework, applicable to a variety of logics, for transforming semantic games first into provability games and finally converting these games into analytic proof systems.