The Journal of Symbolic Logic

Research Article

Games and full completeness for multiplicative linear logic

Samson Abramskya1 and Radha Jagadeesana2

a1 Department of Computing, Imperial College of Science, Technology and Medicine, London, SW7 2BZ, England, E-mail: sa@doc.ic.ac.uk

a2 Department of Mathematical Sciences, Loyola University, Chicago, E-mail: radha@feldberg.math.luc.edu

Abstract

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.

(Received October 06 1992)

(Revised August 10 1993)