semiopedia.org
Linear Logic

Linear Logic

A resource-conscious logical system developed by Jean-Yves Girard that treats propositions as consumable resources rather than persistent truths.

Linear Logic

Linear logic, introduced by Jean-Yves Girard in 1987, represents a fundamental departure from classical logic by treating logical propositions as finite resources that must be managed carefully. Unlike traditional logic where truths persist indefinitely, linear logic tracks how propositions are consumed and transformed during reasoning.

Core Principles

Resource Management

The central insight of linear logic is that logical statements behave like consumable resources:

  • Resources must be used exactly once
  • No implicit weakening or contraction of assumptions
  • Explicit handling of resource duplication and disposal

Connectives

Linear logic introduces new logical connectives:

  • Multiplicative: ⊗ (tensor) and ⅋ (par)
  • Additive: & (with) and ⊕ (plus)
  • Exponential: ! (of course) and ? (why not)

Applications

Computer Science

Linear logic has profound applications in:

Proof Theory

The resource-conscious nature of linear logic has led to advances in:

Variants and Extensions

Several important variants have emerged:

  1. Intuitionistic Linear Logic
  2. Light Linear Logic
  3. Affine Logic

Philosophical Significance

Linear logic provides a novel perspective on:

Historical Context

The development of linear logic represents a significant milestone in the evolution of mathematical logic. It emerged from investigations into coherence spaces and has influenced modern approaches to proof theory and computational logic.

Further Developments

Current research directions include:

The impact of linear logic continues to grow as new applications and theoretical developments emerge in both computer science and mathematical logic.