Symmetric dialogue games in the proof theory of linear logic
Olivier Delande · HAL (Le Centre pour la Communication Scientifique Directe) · 2009
This thesis develops an original approach to the interactive interpretation of the proof theory of linear logic. In contrast with the player/opponent dichotomy commonly associated with game semantics for logic, we propose a model in which the two players have symmetric roles. More precisely, we shift from a situation in which a player aims at proving a goal while the other one aims at refuting it to a situation in which the players aim at proving opposite goals. In the tradition of computation-as-proof-search, each step of the interaction is seen as a step in two orthogonal sequent calculus proof searches. To some extent, this work contributes to formalising the connections between proof search and proof normalisation. We first present a simple symmetric game for the additive fragment of linear logic, as a first introduction to dual proof search. We then introduce a much more involved symmetric game accounting for the multiplicative and additive fragment of linear logic. In order to get a full completeness result, we then develop a third, highly concurrent, symmetric game. Finally, we investigate a few extensions of our model.