A game semantics for linear logic

AbstractWe present a game (or dialogue) semantics in the style of Lorenzen (1959) for Girard's linear logic (1987). Lorenzen suggested that the (constructive) meaning of a proposition ϕ should be specified by telling how to conduct a debate between a proponent P who asserts ϕ and an opponent O who denies ϕ. Thus propositions are interpreted as games, connectives (almost) as operations on games, and validity as existence of a winning strategy for P. (The qualifier ‘almost’ will be discussed later when more details have been presented.) We propose that the connectives of linear logic can be naturally interpreted as the operations on games introduced for entirely different purposes by Blass (1972). We show that affine logic, i.e., linear logic plus the rule of weakening, is sound for this interpretation. We also obtain a completeness theorem for the additive fragment of affine logic, but we show that completeness fails for the multiplicative fragment. On the other hand, for the multiplicative fragment, we obtain a simple characterization of game-semantical validity in terms of classical tautologies. An analysis of the failure of completeness for the multiplicative fragment leads to the conclusion that the game interpretation of the connective ⊗ is weaker than the interpretation implicit in Girard's proof rules; we discuss the differences between the two interpretations and their relative advantages and disadvantages. Finally, we discuss how Gödel's Dialectica interpretation (1958), which was connected to linear logic by de Paiva (1989), fits with game semantics