linear logic
Table of Contents
Linear logic is an alternative logic that, in a certain sense, deals with resources rather than truth.
1. Motivation
The original motivation behind linear logic is very different from the now-common “logic of resources” intuition.
Jean-Yves Girard started with the question: why exactly is the sequent calculus of classical logic not constructive, while the sequent calculi of minimal logic and intuitionistic logic are?
Now, what is the meaning of the separation ? The classical answer is “to separate positive and negative occurrences”. This is factually true but shallow; we shall get a better answer by asking a better question: what in the essence of makes the two latter logics more constructive than the classical one?
(Here, we are taking it as given that a logic has a “natural” sequent calculus.
Girard finds the answer by asking why
2. The connectives
2.1. Simultaneous conjunction
Also called multiplicative conjunction, is the most obvious notion of “linear conjunction”. In order to form it, we need to have both and , each depending on its own list of assumptions.
Unlike with classical conjunction, we cannot simply project out a single component, because then we would have “unused” assumptions corresponding to the “unused” component. Instead, we must ensure that and are both used, thus ensuring that all assumptions are used.
2.2. Alternative conjunction
This seems impossible—haven't we duplicated the assumptions in ? The answer is: only as long as we are allowed to actually “use” both facts later. The elimination rules for do not allow this.
Instead of being allowed to use both and , we must choose one.