Substructural Logics

A sequent has a list of formulas on each side, and three rules govern the lists rather than the formulas in them. They permit adding a formula that is not used, using a formula twice where it appears once, and reordering. They look like bookkeeping, and Gentzen presented them as such.

They are not bookkeeping. Each one encodes an assumption about what a premise is, and dropping any of them produces a logic with different theorems and a different subject matter.

The three rules

Each rule corresponds to something on the computational side of the previous article. Weakening is discarding a value; contraction is copying one; exchange is reordering arguments. A calculus without weakening and contraction is one in which every value is used exactly once, which is the discipline a language for memory or for physical resources would need, and the connection is exact rather than suggestive.

Linear logic

The splitting is the substance of the system. Classically, conjunction introduction from $\Gamma \vdash \varphi$ and $\Gamma \vdash \psi$ requires the two premises to share a context, which is contraction, while combining disjoint contexts gives a different rule. With contraction available the two rules are interderivable and define one connective. Without it they define two: the multiplicative conjunction, written with a tensor, means having both resources, and the additive conjunction means being able to choose either one but not both.

Girard's illustration is a vending machine. One unit of currency and the multiplicative conjunction of a drink and a snack means both are dispensed, which is false of the machine. One unit and the additive conjunction means the buyer chooses, which is true. Classical logic cannot state the difference because it identifies the connectives.

The expressive power that was lost returns in a controlled form through the exponentials, modal operators marking a formula as reusable. A formula under the exponential may be weakened and contracted, so classical and intuitionistic logic embed into linear logic by placing exponentials at the right positions. Nothing is given up; the structural rules become explicit rather than implicit, which is the point. Linear logic has cut elimination, and its proof nets give a representation of proofs that quotients away the irrelevant ordering of rule applications, a problem natural deduction has and does not solve.

The applications followed quickly and are concrete. Session types for communication protocols, where a channel is used according to a schedule and reuse is a bug; the ownership discipline of the Rust programming language, in which a value has one owner and copying must be requested; quantum computation, where the no-cloning theorem is the failure of contraction stated in physics.

The Lambek calculus

The application is grammar, and it is the earliest substructural logic by three decades. A category is assigned to each word: a name gets the basic category for noun phrases, an intransitive verb gets the category that combines with a noun phrase on its left to make a sentence, a transitive verb gets one seeking a noun phrase on its right and then on its left. A string is grammatical when its sequence of categories derives the sentence category. Word order is carried by the directionality of the implications, which is exactly what the absence of exchange makes available.

The framework is the origin of categorial grammar as practised now, and the connection to the previous article is direct: a derivation in the calculus is a term, so the syntactic analysis of a sentence delivers a semantic composition for free. Montague's programme of compositional semantics has this as its natural proof theory, and the pairing of a categorial derivation with a lambda term is how the two are usually presented together.

Next

Dropping weakening is what relevance logic does, and its motivation is not resources but the demand that a premise bear on its conclusion. That demand collides with one of the most familiar arguments in classical logic, and the collision has been the subject of a long dispute.