View source for 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 [[Process Calculus|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 [[Concurrency Theory|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|affine logic]]''' (which allows weakening but not contraction), '''[[Non-Commutative Linear Logic|non-commutative linear logic]]''' (which tracks the order of resources), and '''[[Differential Linear Logic|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.

[[Category:Logic]]
[[Category:Computer Science]]
[[Category:Systems]]