Contraction-free Proofs and Finitary Games for Linear Logic

In the standard sequent presentations of Girard's Linear Logic [Girard, J.-Y., Linear logic, Theoretical Computer Science 50 (1987), pp. 1–102] (LL), there are two “non-decreasing” rules, where the premises are not smaller than the conclusion, namely the cut and the contraction rules. It is a universal concern to eliminate the cut rule. We show that, using an admissible modification of the tensor rule, contractions can be eliminated, and that cuts can be simultaneously limited to a single initial occurrence. This view leads to a consistent, but incomplete game model for LL with exponentials, which is finitary, in the sense that each play is finite. The game is based on a set of inference rules which does not enjoy cut elimination. Nevertheless, the cut rule is valid in the model.