Linear Logic

Origin. Girard (1987). Resource-sensitive logic. Formulas as resources, used exactly once. Multiplicative/additive distinction. Foundation for concurrency, quantum, and programming language theory.

Models. Formulas are resources. Use once unless marked reusable. Multiplicatives: tensor ⊗, par ⅋. Additives: with &, plus ⊕. Exponentials: ! (of course), ? (why not). Coherence spaces, phase semantics.

Formalism.

Connectives: Multiplicative conjunction: A ⊗ B (both, independently) Multiplicative disjunction: A ⅋ B (par) Additive conjunction: A & B (external choice) Additive disjunction: A ⊕ B (internal choice) Linear implication: A ⊸ B (consume A, produce B)

Exponentials: !A: unlimited copies of A (of course) ?A: demand for A (why not) !A ⊸ A (dereliction) !A ⊸ !A ⊗ !A (contraction) !A ⊸ 1 (weakening)

Units: 1: multiplicative true ⊥: multiplicative false (dual of 1) ⊤: additive true 0: additive false

Negation: A⊥: linear negation (involutive: A⊥⊥ = A) De Morgan: (A ⊗ B)⊥ = A⊥ ⅋ B⊥

Sequent calculus: ⊢ Γ (one-sided sequents) Formulas as resources in multiset.

Key rules: ⊢ A, Γ ⊢ A⊥, Δ ─────────────────── cut ⊢ Γ, Δ

⊢ A, B, Γ ─────────── ⅋ ⊢ A ⅋ B, Γ

⊢ A, Γ ⊢ B, Δ ───────────────── ⊗ ⊢ A ⊗ B, Γ, Δ

Symbols.

Metatheory. Girard (1987) proved cut elimination for full linear logic, propositional and first-order, and derived the subformula property and consistency from it. The decision problems separate sharply by fragment: multiplicative linear logic MLL is NP-complete (Kanovich), the multiplicative–additive fragment MALL is PSPACE-complete, and provability in full propositional linear logic with the exponentials is undecidable, by reduction from and-branching two-counter machines (Lincoln, Mitchell, Scedrov and Shankar 1992); the decidability of the multiplicative–exponential fragment MELL has been open since the 1990s. Phase semantics is sound and complete for provability, while coherence spaces model proofs rather than provability. Proof nets give a sequentialization-free representation of MLL derivations: a proof structure is a proof net exactly when it satisfies Girard's long-trip criterion, equivalently the Danos–Regnier condition that every switching graph be acyclic and connected. Girard's translation of intuitionistic implication as !A ⊸ B is faithful, so linear logic refines intuitionistic logic rather than merely restricting it.

Applies to. Concurrency (session types). Quantum computing. Game semantics. Separation logic foundations. Resource management.

Limitations. Weakening and contraction are unavailable, so a hypothesis can be neither discarded nor duplicated; recovering them requires the exponentials, and with them provability becomes undecidable. The deduction theorem holds for ⊸ only in its linear form: Γ, A ⊢ B and Γ ⊢ A ⊸ B are interchangeable, but a hypothesis available for repeated use yields only ⊢ !A ⊸ B, not ⊢ A ⊸ B. The exponentials are not canonical — the sequent rules for ! do not determine it up to isomorphism, so two modalities with the same rules need not be provably equivalent, and ! is not a universal construction supplied by the calculus. Proof nets are satisfactory only for the multiplicative fragment; the additives force boxes or slices, and no comparably simple correctness criterion covers full linear logic. Phase semantics is complete for provability but identifies all proofs of a formula, so it cannot serve as a semantics of proofs.

© 2026 Lingenic LLC