Linear Logic

Linear logic is a substructural logic created by Jean-Yves Girard in 1987 that makes the management of logical resources explicit. Unlike classical logic, where premises can be freely duplicated or discarded, linear logic treats each premise as a consumable resource that must be used exactly once unless explicitly marked as reusable via the exponential modalities ! (of course) and ? (why not). This resource-sensitivity makes linear logic a natural logical foundation for concurrent computation, where processes consume and transform resources through interaction, and for the semantics of programming languages with explicit state and memory management.

The central insight of linear logic is that the logical rules for implication and conjunction have two distinct forms — an additive form that corresponds to choice and a multiplicative form that corresponds to parallel composition — and that classical and intuitionistic logic arise as special cases where these distinctions are collapsed. The cut-elimination procedure in linear logic corresponds precisely to the evaluation of processes in a concurrent system, revealing that logical deduction and concurrent computation are not merely analogous but structurally identical at the level of proof dynamics.

Linear logic has spawned numerous variants and applications, including affine logic (which allows weakening but not contraction), non-commutative linear logic (which tracks the order of resources), and differential linear logic, which introduces differentiation and integration of proofs. These developments suggest that linear logic is not merely a specialized logic for computer scientists but a more fundamental logical framework from which classical logic is the degenerate case — the limit where resources become infinitely abundant.