We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a (...) natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass, et al. (shrink)

We present a game semantics in the style of Lorenzen for Girard's linear logic . Lorenzen suggested that the 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 as operations on games, and validity as existence of a winning strategy for P. We propose that the connectives of linear logic can be naturally interpreted as the (...) operations on games introduced for entirely different purposes by Blass . 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 , which was connected to linear logic by de Paiva , fits with game semantics. (shrink)