---
tag: 2P2184B6HE
kind: concept
name: Linear logic
msc: [03B47, 03F52]
sources:
  - url: https://en.wikipedia.org/wiki/Linear_logic
same_as:
  wikidata: Q841728
  wikipedia: Linear logic
---

## Summary

Linear logic, introduced by Jean-Yves Girard in 1987, is a logic in which hypotheses are resources that must be used exactly once.
It drops the structural rules of weakening and contraction, and allows them back only for formulas marked with the exponentials $!$ and $?$.
As a result, conjunction and disjunction split into multiplicative and additive versions.
It has applications in proof theory, the semantics of programming languages and the theory of concurrency.

## Explanations

### L1 human

In ordinary logic, a hypothesis can be used as often as you like, or not at all.
In linear logic, using a hypothesis consumes it, like spending a coin.
With one euro you can buy a coffee, and with one euro you can buy a tea, but one euro does not buy both.
Linear logic has a separate connective for each of these situations: "I can choose either" and "I have both at once".