Contraction-free proofs and finitary games for Linear Logic
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.
Keywords
Cite
@article{arxiv.0905.4064,
title = {Contraction-free proofs and finitary games for Linear Logic},
author = {André Hirschowitz and Michel Hirschowitz and Tom Hirschowitz},
journal= {arXiv preprint arXiv:0905.4064},
year = {2009}
}
Comments
19 pages, uses tikz and Paul Taylor's diagrams