Linear logic
Name | Connectives | Categorical semantics |
---|---|---|
Multiplicative linear logic without negation | \(\otimes\), \(⅋\), \(1\), \(\bot\) | Linearly distributive categories |
Multiplicative linear logic (MLL) | \(\otimes\), \(⅋\), \(1\), \(\bot\), \((-)^\bot\) | *-autonomous categories |
Multiplicative intuitionistic linear logic (MILL) | \(\otimes\), \(1\), \(\multimap\) | Closed monoidal categories |
(Classical) linear logic | \(\&\), \(\oplus\), \(\top\), \(0\), \(\otimes\), \(⅋\), \(1\), \(\bot\), \((-)^\bot\), \(!\), \(?\) |
The nLab lists more variants of linear logic.
Logical system of linear logic
Linear logic is a logical system invented by Jean-Yves Girard:
- Girard, 1987: Linear logic (doi)
- Seminal paper introducing linear logic and proof nets
- Girard, 1995: Linear logic: its syntax and semantics (pdf)
Girard has also exposited linear logic in his books, in his distinctive (sometimes incomprehensible) style:
- Girard, 1989: Proofs and Types (pdf), Appendix B: What is linear logic?
- Appendix B is actually written by Yves Lafont
- Girard, 2011: Lectures on Logic (doi), Part III: Linear logic
By now there are many surveys of linear logic, written from different perspectives:
- For logicians:
- For proof theorists:
- Troelstra, 1992, via CSLI: Lectures on linear logic
- Troelstra & Schwichtenberg, 2000: Basic proof theory, Ch. 9: Modal and linear logic (doi)
- For philosophers: Di Cosmo & Miller, 2006, in SEP: Linear logic
- For programming language theorists:
- For linguists: Crouch & Genabith, 2000: Linear logic for linguists (pdf)
- For category theorists: see “categorical semantics” below
- For algebraists: Murfet, 2014: Logic and linear algebra: an introduction (arxiv)
Categorical semantics of linear logic
Several surveys aim to present a holistic view of linear logic’s categorical semantics:
- Schalk, 2004: What is a categorical model for linear logic? (pdf)
- Mellies, 2006: Categorical semantics of linear logic: A survey (pdf)
- de Paiva, 2014: Categorical semantics of linear logic for all (doi, pdf)
The main references for linearly distributive categories are the original papers by Hyland & de Paiva and by Cockett and Seely. Linearly distributive categories were originally called “weakly distributive categories” because, although they do not weaken classical distributivity in the obvious way that rig categories do, a cartesian monoidal category that is weakly distribtive is classically distributive.
- Hyland & de Paiva, 1993: Full intuitionistic linear logic (extended abstract) (doi)
- Benton, Bierman, de Paiva, Hyland, 1993: A term calculus for intuitionistic linear logic (doi, pdf)
- Cockett & Seely, 1997: Weakly distributive categories (doi)
- Conference version in 1992 (doi)
- Cockett & Seely, 1999: Linearly distributive functors (doi)
- Blute, Cockett, Seely, Trimble, 1996: Natural deduction and coherence for
weakly distributive categories (doi)
- Introduces a graphical language for Girard’s proof nets reminiscent of string diagrams
- Language rules are quite complicated due to presence of units