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.

Symbol	Unicode	Name	Meaning
⊗	U+2297	Tensor	Multiplicative and
⅋	U+214B	Par	Multiplicative or
&	U+0026	With	Additive and
⊕	U+2295	Plus	Additive or
⊸	U+22B8	Lollipop	Linear implication
!	—	Bang	Of course
?	—	Question	Why not
⊥	U+22A5	Bottom	Linear false

Metatheory. Cut elimination. Proof nets for MLL. Phase semantics. Coherence spaces. Geometry of interaction. Decidable (propositional MLL).

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

Limitations. Complex. Multiple fragments. Exponentials subtle. Learning curve steep.