Linear logic
Linear logic, introduced by mathematician Jean-Yves Girard, is a kind of substructural logic that denies the structural rules of weakening and contraction for all hypotheses. Linear hypotheses therefore have a natural resource interpretation: every hypothesis must be consumed exactly once in a proof. The logical connectives must be re-examined in this interpretation; each connective splits into multiplicative and additive versions.
Conjunction divides into:
- Multiplicative conjunction, aka. tensor (written ⊗). The unit of tensor is one (written 1); i.e., A ⊗ 1 ≡ A.
- Additive conjunction, aka. internal choice or with (written &). The unit of with is top.
Disjunction divides into:
- Multiplicative disjunction, aka. par (written using an inverted ampersand), with unit bottom (written ⊥).
- Additive disjunciton, aka. external choice (written ⊕), with unit zero (written 0).
Ordinary logic is embedded in linear logic by a pair of exponential modalities (see modal logic).
- Contraction is allowed for the bang exponential operator (written !). Two occurrences of !A (for proposition A) as hypotheses may be contracted into a single occurrence.
- Weakening is allowed for the question mark operator (written ?). Any fact can be weakened by an additional conclusion ?A.
Under the resource interpretation, ! encodes arbitrary production and ? encodes arbitrary consumption.
Flavours of linear logic
Linear logic has many variants. The primary axis of variation is along the classical/intuitionistic divide:
- Classical linear logic (CLL) is the original linear logic as proposed by Girard. In CLL every connective has a dual.
- Intuitionistic linear logic (ILL) allows only a single conclusion. Unlike CLL, connectives in ILL do not have perfect duals. Indeed, the connectives par and question mark, and the propositional constant bottom (⊥), are absent in ILL because their introduction requires multiple conclusions.
Other variants of linear logic variously allow or disallow certain connectives, giving rise to logics with varying complexity. The following are the most common variants.
- Multiplicative linear logic or MLL. This variant allows only the multiplicative connectives tensor and par (and their units). It is decidable, but the decision problem is NP complete.
- Multiplicative additive linear logic or MALL, which adds the additive connectives to MLL. This variant is also decidable with a PSPACE complete decision problem.
- Multiplicative exponential linear logic or MELL, which is MLL plus the exponential operators. The decision problem for MELL is currently open.
- Multiplicative additive exponential linear logic or MAELL, which has all the above connectives. This variant is undecidable.
There are also first- and higher-order extensions of linear logic, but their development is standard (See first-order logic and higher-order logic.)
The closest sub-structural cousins of linear logic are:
- Affine logic, which extends linear logic with the structural rule of weakening. The connectives one and top are indistinguishable in affine logic.
- Strict logic or relevant logic, which extends linear logic with the structural rule of contraction.
- Non-commutative logic or ordered logic which removes the structural rule of exchange from linear logic. Multiplicative conjunction divides further into a pair of fuses (left fuse and right fuse).