nLab
linear logic

Idea

Unlike traditional logics, which deal with the truth of propositions, linear logic is often described as dealing with the availability of resources. A proposition, if it is true, remains true no matter how we use that fact in proving other propositions. By contrast, in using a resource $A$ to make available a resource $B$, $A$ itself may be consumed or otherwise modified. Linear logic deals with this by restricting our ability to duplicate or discard resources freely. For example, we have

$$\text{have cake}⊢\text{eat cake}$$\text{have cake}\vdash\text{eat cake}

from which we can prove

$$\text{have cake},\text{have cake}⊢\text{have cake}\wedge \text{eat cake}$$\text{have cake},\text{have cake}\vdash \text{have cake}\wedge \text{eat cake}

which by left contraction (duplication of inputs) in classical logic yields

$$\text{have cake}⊢\text{have cake}\wedge \text{eat cake}$$\text{have cake}\vdash\text{have cake}\wedge\text{eat cake}

Linear logic would disallow the contraction step and treat $\text{have cake},\text{have cake}⊢A$ as explicitly meaning that two slices of cake yield $A$. Disallowing contraction then corresponds to the fact that we can’t turn one slice of cake into two (more’s the pity), so you can't have your cake and eat it too.

Linear logic was introduced in [1]. Although it is usually presented in terms of inference rules, it was apparently discovered by Girard while studying coherent spaces (not the topological kind).

Discussion

Probably the best way to explain LL to a category theorist is to say that its models are *-autonomous categories with extra structure (see [2]).

Firstly, there is a monoidal ‘tensor’ connective $A\otimes B$. Negation $A^{\perp }$ is modelled by the duality involution $(-{)}^{*}$, while linear implication $A⊸B$ corresponds to the internal hom, which can be defined as $(A\otimes B^{\perp }{)}^{\perp }$. There is a De Morgan dual of the tensor called ‘par’, with $A⅋B=(A^{\perp }\otimes B^{\perp }{)}^{\perp }$. Tensor and par are the ‘multiplicative’ connectives, which roughly speaking represent the parallel availability of resources.

The ‘additive’ connectives $\&$ and $\oplus$, which correspond in another way to traditional conjunction and disjunction, are modelled as usual by products and coproducts. Seely notes [2] that products are sufficient, as $*$-autonomy then guarantees the existence of coproducts; that is, they are also linked by de Morgan duality.

LL recaptures the notion of a resource that can be discarded or copied arbitrarily by the use of the modal operator $!$: $!A$ denotes an ’$A$-factory’, a resource that can produce zero or more $A$s on demand. It is modelled using a comonad $!$ on the underlying $*$-autonomous category that is (symmetric) monoidal, in the sense that there is an isomorphism $!A\otimes !B\cong !(A\times B)$. Since every $A$ is canonically a symmetric $\times$-comonoid, $!A$ is then a symmetric $\otimes$-comonoid.

An LL sequent

$$A_1,\dots ,A_n⊢B_1,\dots ,B_m$$A_1,\ldots,A_n \vdash B_1,\ldots,B_m

is interpreted as a morphism

$${\otimes }_i{A}_i\to {⅋}_j{B}_j$$\otimes_i A_i \to \parr_j B_j

The comonoid structure on $!A$ then yields the weakening

$$\Gamma \otimes !A\to \Gamma \otimes I\to \Gamma$$\Gamma\otimes !A \to \Gamma \otimes I \to \Gamma

and contraction

$$\Gamma \otimes !A\to \Gamma \otimes !A\otimes !A$$\Gamma\otimes !A \to \Gamma \otimes !A \otimes !A

maps. The corresponding rules are interpreted by precomposing the interpretation of a sequent with one of these maps.

The (co)Kleisli category of $!$ is cartesian closed, and the product there coincides with the product in the base category. The exponential (unsurprisingly for a Kleisli category) is $B^A\cong !A⊸B$.

References

1. Girard, Jean-Yves, ‘Linear logic’. Theoretical Computer Science 50:1, 1987.

2. Seely, R. A. G., ‘Linear logic, $*$-autonomous categories and cofree coalgebras’, Contemporary Mathematics 92, 1989. Available at http://www.math.mcgill.ca/rags/nets/llsac.ps.gz.

3. The article on the English Wikipedia has good summaries of the meanings of the logical operators and of the commonly studied fragments.