Notes on Girard's Linear Logic

🔗 Linear logic (1987) - Girard

Jean-Yves Girard’s 1987 paper introduced linear logic as a refinement of classical and intuitionistic logic that tracks resource usage. Unlike traditional logics where assumptions can be used arbitrarily many times, linear logic treats propositions as consumable resources.

The Resource Problem

Classical logic allows the structural rules of weakening (adding unused assumptions) and contraction (duplicating assumptions). This creates an idealized world where information is free and infinitely copyable. Girard observed that many computational processes—memory allocation, concurrent communication, quantum states—don’t behave this way.

Linear logic removes these structural rules by default, making every assumption precious. If you have proposition $A$, you can use it exactly once unless explicitly marked otherwise.

The Exponentials

The key innovation is the exponential modalities:

• !A (“of course A”): Recovers classical behaviour, allowing unlimited use
• ?A (“why not A”): Dual to !A

These modalities let you opt into classical reasoning where needed while maintaining resource consciousness elsewhere.

New Connectives

Linear logic distinguishes between two kinds of “and” and “or”:

Multiplicative connectives (consume resources together):

• A ⊗ B: Multiplicative “and” (tensor)
• A ⅋ B: Multiplicative “or” (par)

Additive connectives (represent choice):

• $A \mathbin{\&} B$: Additive “and” (with) - you can choose to use either $A$ or $B$
• $A ⊕ B$: Additive “or” (plus) - external choice between $A$ or $B$

Proof Nets

Beyond sequent calculus, Girard introduced proof nets: graphical representations of proofs that eliminate bureaucratic details of proof trees. These reveal the essential structure of logical reasoning and influenced later work in geometry of interaction.

Impact and Applications

Linear logic has found applications far beyond its logical origins:

• Programming languages: Session types, ownership systems (like Rust), and resource-aware functional languages
• Concurrency: Process calculi where communication channels are linear resources
• Quantum computing: Quantum states cannot be cloned, making them naturally linear
• Game semantics: Players have limited resources in logical games

The Deeper Insight

Girard’s work shows that classical logic’s “structural” rules aren’t just convenient bookkeeping. Rather, they encode deep assumptions about the nature of information and computation. By questioning these assumptions, linear logic opens new ways to think about proof, program, and process.

The paper demonstrates that logic isn’t just about truth and falsity, but about how we use logical resources. This shift from static truth to dynamic process has influenced decades of research in theoretical computer science and continues to shape how we understand the relationship between logic and computation.