Contraction-free proofs and finitary games for linear logic

DOI10.1016/J.ENTCS.2009.07.095MaRDI QIDQ2805162zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

contraction eliminationgame semanticslinear logic

Mathematics Subject Classification ID

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

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.

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

Cites work

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

Cited in

(4)

• Finite games for a predicate logic without contractions
• Contraction-free proofs and finitary games for linear logic
• Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract)
• Saturated formulas in full 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)