Contraction-free proofs and finitary games for Linear Logic

TL;DR

This paper introduces a contraction-free proof system for Linear Logic using a modified tensor rule, resulting in a finitary game model where cuts are limited but still valid, simplifying proof analysis.

Contribution

It presents a novel approach to eliminate contraction and limit cuts in Linear Logic proofs through rule modifications, leading to a finitary game model.

Findings

Contraction can be eliminated via an admissible tensor rule modification.

Cuts can be limited to a single initial occurrence.

The resulting game model is finitary and consistent, with cuts valid within the model.

Abstract

In the standard sequent presentations of Girard's Linear Logic (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.