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)

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)

The main concern of this paper is the design of a noetherian and confluent normalization for LK 2. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic ; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic using (...) appropriate embeddings ; it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making. A comparison of our method to that of embedding LK into LJ brings to the fore the latter's defects for these `deconstructive purposes'. (shrink)