Contraction-free proofs and finitary games for linear logic

DOI10.1016/J.ENTCS.2009.07.095zbMATH Open1337.03088arXiv0905.4064OpenAlexW2150101840MaRDI QIDQ2805162FDOQ2805162

Authors: Michel Hirschowitz, Tom Hirschowitz, André Hirschowitz 

Publication date: 10 May 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/0905.4064

Recommendations

• A game semantics for linear logic
• Some semantical aspects of linear logic
• scientific article; zbMATH DE number 1497810
• Games and full completeness for multiplicative linear logic
• Finite games for a predicate logic without contractions

zbMATH Keywords

game semanticslinear logiccontraction elimination

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cites Work

• Linear logic
• Locus solum: From the rules of logic to the logic of rules.
• A Theory for Game Theories
• A game semantics for linear logic
• Games and full completeness for multiplicative linear logic
• The linear abstract machine
• Contraction-free sequent calculi for intuitionistic logic
• Normalization without reducibility
• A short proof of the strong normalization of classical natural deduction with disjunction
• Contraction-elimination for implicational logics
• Corrigenda to: ``The linear abstract machine
• Contraction-free proofs and finitary games for linear logic
• Admissibility of structural rules for extensions of contraction-free sequent calculi

Cited In (3)

• Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract)
• Finite games for a predicate logic without contractions
• Contraction-free proofs and finitary games for linear logic

This page was built for publication: Contraction-free proofs and finitary games for linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2805162)