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	Linear implication	Consume premise
⊗	U+2297	Tensor/Fusion	Multiplicative and
&	—	With	Additive and
*	—	Separating conjunction	Disjoint combination
—*	—	Magic wand	Separating implication
·	—	Lambek product	Ordered concatenation
\ /	—	Lambek slashes	Directional implication
→	U+2192	Relevant implication	Relevance-requiring
∘	U+2218	Fusion	Relevant conjunction

Metatheory. Substructural logics form a lattice ordered by which rules are present. Algebraic semantics: residuated lattices, quantales, Lambek algebras. Cut elimination typically holds. Complexity varies: Lambek calculus is NP-complete; full linear logic is undecidable. Categorical semantics: monoidal categories, *-autonomous categories.

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. More complex than classical logic. Each variant sacrifices different classical reasoning. Choosing the right substructural logic requires matching the application. The zoo of systems can be overwhelming. Some practical applications (like separation logic) use only fragments.