# Linear logic

[https://en.wikipedia.org/wiki/Linear\_logic](https://en.wikipedia.org/wiki/Linear_logic) [https://plato.stanford.edu/entries/logic-linear/](https://plato.stanford.edu/entries/logic-linear/) [https://ncatlab.org/nlab/show/linear+logic](https://ncatlab.org/nlab/show/linear+logic)

* In classical logic, `φ ⊢ ψ` means that given the truth of φ, you can conclude that ψ is true. Once you have proven that ψ is true, that has no bearing on the truth of φ: that premise is still true just as it ever was. For example, if you have 3 premises `A -> B`, `A -> C`, `A`, you can prove `B` and `C` by _reusing_ `A` premise. So, it is possible to derive: `A -> B, A -> C, A ⊢ B ∨ C`.
* **Linear logic** is a type of _substructural logic_, proposed by Jean-Yves Girard, that restricts the reusing aspect of classical logic wrt premises. In linear logic, each premise **must be used exactly once** to construct the conclusion (it must be used, and it must be used only once).
* Ideas from linear logic have been influential in design of PLs because of its emphasis on the restriction of resources, duality and interaction.
* In proof theory, linear logic derives from an analysis of classical sequent calculus in which the use of structural rules of _contraction_ and _weakening_ are carefully controlled.
* Operationally, this means that logical deduction is no longer merely about collecting persistent "truths", but it is also a way of manipulating resources that cannot freely be duplicated or thrown away.
* In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing _cartesian closed categories_ by _symmetric monoidal categories_, or the interpretation of classical logic by replacing `Boolean algebras` by `C*-algebras`.
* Linear logic is useful for reasoning about resources for each hypothesis must be used exactly once.
* Linear types introduce the new "lollipop" arrow, `⊸` (latex: `\multimap`)

```javascript
Syntax          Meaning

F := F ⨂ F      α and β hold simultaneously, α ⊗ β
   | 1          nothing holds
   | F & F      α and β hold but not necessarily simultaneously, α & β
   | ⊤          tautology
   | F ⨁ F      α and β hold, α ⊕ β
   | 0          absurdity
   | F ⊸ F      if α holds then β holds, α ⊸ β
   | !F         α holds arbitrarily often, !α
```
