Linear Logic Properly Displayed
Giuseppe Greco, Alessandra Palmigiano

TL;DR
This paper develops proper display calculi for various linear logics, ensuring soundness, completeness, and cut-elimination, and introduces a Lambek calculus variant with controlled exchange and associativity.
Contribution
It presents the first proper display calculi for linear logics with exponentials, emphasizing the importance of properness for cut-elimination and proof-theoretic properties.
Findings
Proper display calculi are sound and complete for linear logics.
Cut-elimination is smoothly achieved due to properness.
A new Lambek calculus variant with exponentials is introduced.
Abstract
We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut-elimination and subformula property. Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest proof of cut-elimination. Our proposal builds on an algebraic and order-theoretic analysis of linear logic, and applies the guidelines of the multi-type methodology in the design of display calculi.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
