Substructural Logics

Origin. Identified through Gentzen's sequent calculus (1934) by analyzing structural rules. Lambek calculus for linguistics (1958). Relevance logic (Anderson & Belnap, 1960s-70s) rejected irrelevant implications. Linear logic (Girard, 1987) rejected contraction and weakening. Unified perspective emerged recognizing the family structure.

Models. Logics that restrict or modify structural rules of sequent calculus. The structural rules (weakening, contraction, exchange, associativity) govern how contexts behave. Dropping or modifying them gives different logics with different resource/relevance/order sensitivities.

Formalism.

Structural rules in sequent calculus:

Weakening (W): Γ ⊢ A implies Γ, B ⊢ A "Can add unused premises" Rejected in: linear, relevant, Lambek

Contraction (C): Γ, A, A ⊢ B implies Γ, A ⊢ B "Can reuse premises" Rejected in: linear, affine, Lambek

Exchange (E): Γ, A, B, Δ ⊢ C implies Γ, B, A, Δ ⊢ C "Order doesn't matter" Rejected in: Lambek, non-commutative linear

Associativity: How premises group Rejected in: some non-associative logics

The substructural zoo:

Logic	W	C	E	Key Feature
Classical	✓	✓	✓	Full structural
Affine	✓	✗	✓	Use at most once
Relevant	✗	✓	✓	Must use everything
Linear	✗	✗	✓	Use exactly once
Lambek	✗	✗	✗	Order-sensitive

Relevant logic (R): Requires relevance between antecedent and consequent A → (B → A) not valid (A unconnected to B → A) Blocks "paradoxes of implication"

Affine logic: Can discard but not duplicate Models resources that can be wasted Weaker than linear

Lambek calculus: Non-commutative, non-contractive, no weakening Product A · B means "A then B" Models syntactic concatenation in linguistics

Bunched implications (BI): Combines linear and intuitionistic implication Basis for separation logic Two conjunctions: * (separating) and ∧ (sharing)

Symbols.

Symbol	Unicode	Name	Meaning
⊸	U+22B8	Multimap / Lollipop	Linear implication, consumes its premise
⊗	U+2297	Circled times / Tensor	Multiplicative conjunction
&	U+0026	Ampersand / With	Additive conjunction
*	U+002A	Asterisk / Separating conjunction	Disjoint combination in BI
·	U+00B7	Middle dot / Lambek product	Ordered concatenation, "A then B"
\	U+005C	Reverse solidus / Under	Left Lambek residual
/	U+002F	Solidus / Over	Right Lambek residual
→	U+2192	Rightwards arrow	Relevant implication
∘	U+2218	Ring operator / Fusion	Relevant intensional conjunction
∧	U+2227	Logical and	Extensional conjunction, the sharing conjunction of BI
⊢	U+22A2	Right tack / Turnstile	Sequent arrow
Γ	U+0393	Gamma / Context	Structured antecedent of a sequent
Δ	U+0394	Delta / Context	Second context in the exchange rule
✓	U+2713	Check mark	Structural rule present
✗	U+2717	Ballot X	Structural rule absent
—*	—	Magic wand	Separating implication of BI
W	—	Weakening	Γ ⊢ A gives Γ, B ⊢ A
C	—	Contraction	Γ, A, A ⊢ B gives Γ, A ⊢ B
E	—	Exchange	Permutation of the context
FL	—	Full Lambek calculus	The common base of the family
BI	—	Bunched implications	Linear and intuitionistic implication together

Metatheory. The family is organized by the Full Lambek calculus FL: substructural logics are the axiomatic extensions of FL, and the lattice of such extensions is dually isomorphic to the lattice of subvarieties of FL-algebras — pointed residuated lattices — which is the algebraization Galatos, Jipsen, Kowalski and Ono set out in Residuated Lattices: An Algebraic Glimpse at Substructural Logics (2007). Cut elimination holds for FL and for its extensions by exchange, weakening and contraction taken as sequent rules, and the subformula property follows. Decidability is not uniform across the family: FL, FLe, FLw and FLew are decidable, the last by the finite embeddability property (Blok and van Alten 2002), while full propositional linear logic is undecidable and MALL is PSPACE-complete (Lincoln, Mitchell, Scedrov and Shankar 1992), and R, E and T are undecidable (Urquhart 1984). Derivability in the Lambek calculus is NP-complete (Pentus 2006), and the Lambek grammars generate exactly the context-free languages (Pentus 1993). Categorically, monoidal biclosed categories model the Lambek calculus, symmetric monoidal closed categories model intuitionistic linear logic, and *-autonomous categories model the classical version.

Applies to. Linguistics (Lambek calculus for syntax). Resource reasoning (linear). Program verification (separation logic). Relevance in inference (relevant logic). Concurrency (linear, BI). Type systems with resource tracking.

Limitations. Which structural rules are dropped does not determine the logic. Once contraction and weakening go, each connective splits into a multiplicative and an additive form, and whether the additives distribute is an independent choice the structural-rule table does not record: linear logic's do not and R's extensional connectives do, though neither has weakening for the arrow. Distribution is also where the proof theory breaks down — it is not derivable in FL, and adding it as an axiom loses the cut-free sequent formulation, so R requires display or hypersequent machinery instead. The family has no common decision procedure: contraction together with distribution yields the undecidable R, E and T, and exponentials yield undecidable linear logic. Craig interpolation fails for R, E and T (Urquhart 1993). The deduction theorem survives only in modified forms, and disjunctive syllogism is unavailable inside the implication throughout the relevant and linear branches.