Intuitionistic Linear Logic (ILL)

Origin. Implicit in Girard (1987) as the intuitionistic fragment; Girard and Lafont, "Linear logic and lazy computation" (1987), gave the first term calculus; Benton, Bierman, de Paiva, and Hyland, "A term calculus for intuitionistic linear logic" (1993), gave the one that stuck, and Bierman's thesis (1994) the categorical semantics. Hyland and de Paiva's FILL (1993) is the full-intuitionistic variant.

Models. Linear logic with one conclusion. Girard's LL is classical — involutive negation, ⅋, ?, and a two-sided duality — and it is beautiful and has no term calculus, because a proof with many conclusions is not a program. ILL drops ⅋, ⊥, and ?, makes ⊸ primitive rather than defined, and gets Curry–Howard back. Everything that uses linear logic in computing uses ILL.

Formalism.

Connectives: ⊗ tensor, ⊸ linear implication (primitive), & with, ⊕ plus, ! of course, 1, ⊤, 0. Absent: ⅋, ⊥, ?, and the involutive (−)⊥. Linear negation is not primitive: ¬A is A ⊸ 0, and it is not involutive.

Sequents: Γ ⊢ A — one conclusion, as in LJ. Γ is a multiset: exchange yes, weakening and contraction no.

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

Γ, A ⊢ B ──────────── ⊸R Γ ⊢ A ⊸ B

!Γ ⊢ A ──────── !R (promotion: the context must be entirely !'d) !Γ ⊢ !A

The exponential's three rules: dereliction !A ⊢ A weakening Γ ⊢ B ⟹ Γ, !A ⊢ B contraction Γ, !A, !A ⊢ B ⟹ Γ, !A ⊢ B ! is exactly the modality that restores the structural rules, for the formulas that carry it.

Term calculus (Benton–Bierman–de Paiva–Hyland): Types are formulas; terms are proofs. ⊗ gives pairs that must both be consumed; & gives pairs of which one is chosen. ! gives promotion/dereliction as a comonadic pair. Subject reduction and strong normalization hold; cut elimination is β-reduction.

Categorical semantics: A symmetric monoidal closed category with finite products and a monoidal comonad for !. The linear–non-linear adjunction (Benton 1995): a monoidal adjunction between a cartesian category and a linear one, whose comonad is !. This is the model that stuck.

ILL vs FILL: FILL (Hyland–de Paiva) keeps ⅋, ⊥, ? and multiple conclusions while staying intuitionistic — all connectives independent, as in IPC. Harder, and less used.

Symbols.

Symbol	Unicode	Name	Meaning
⊸	U+22B8	Linear implication	Primitive here, defined in LL
⊗	U+2297	Tensor	Both, consumed
⊕	U+2295	Plus	One, determined by the proof
⊢	U+22A2	Sequent	One conclusion
⊤	U+22A4	Top	Unit of the additive conjunction &
⅋	U+214B	Par	Multiplicative disjunction; absent from ILL
⊥	U+22A5	Bottom	Unit of ⅋; absent from ILL
¬	U+00AC	Negation	Defined as A ⊸ 0; not involutive
⟹	U+27F9	Rule direction	Premise to conclusion in the exponential rules
Γ	U+0393	Gamma	A context, a multiset of formulas
Δ	U+0394	Delta	A second context in the cut rule
β	U+03B2	Beta	β-reduction, the term-level form of cut elimination
−	U+2212	Placeholder	The argument slot in the involution (−)⊥
&	—	With	Either, chosen
!	—	Of course	Restores weakening and contraction
?	—	Why not	Dual exponential; absent from ILL
1	—	One	Unit of the tensor
0	—	Zero	Unit of ⊕; the target of linear negation

Metatheory. Cut elimination holds for ILL, so the calculus has the subformula property and is consistent, and cut elimination is exactly β-reduction on the Benton–Bierman–de Paiva–Hyland term calculus (1993), which Bierman's thesis (1994) proved confluent and strongly normalizing. Girard's translation of intuitionistic implication as !A ⊸ B is sound and faithful: IPC proves A iff ILL proves its translation, so ILL is a conservative refinement rather than a weakening. The categorical semantics is settled by Benton's linear–non-linear adjunction (1995), a symmetric monoidal adjunction between a cartesian category and a symmetric monoidal closed one; the induced comonad is a linear exponential comonad, and Bierman showed that Seely's original 1989 axioms were insufficient and had to be strengthened to make the comonoid structure compatible with the monoidal comonad. Complexity is fragment-dependent: multiplicative linear logic is NP-complete (Kanovich 1992), MALL is PSPACE-complete (Lincoln, Mitchell, Scedrov and Shankar 1992), and full propositional linear logic with exponentials is undecidable (same authors).

Applies to. Linear and affine type systems. Session types. Quantum programming languages, where no-cloning is the absence of contraction. Bunched implications and separation logic. Any resource discipline with a term calculus — which is all of them.

Limitations. Provability is undecidable once the exponentials are present, so no decision procedure exists for full propositional ILL, and the decidability of the multiplicative-exponential fragment MELL has been open since the 1990s. Linear negation is not involutive: with ¬A defined as A ⊸ 0 the double-negation law fails, ⅋, ⊥ and ? are unavailable, and the De Morgan dualities that organize classical linear logic have no counterpart, so classical linear logic cannot be recovered inside ILL. The exponential is extra structure rather than a universal construction — a linear exponential comonad has to be supplied, and the characterization of ! as the cofree commutative comonoid needs further completeness assumptions on the category. The multiplicative and additive layers do not distribute, so there is no normal form combining ⊗ and &. Multiple-conclusion intuitionistic variants are delicate: Hyland and de Paiva's FILL required a side condition on the ⅋ rule that Bierman (1996) showed the original cut-elimination argument had missed.