Linear Logic

logic

Definition

Linear Logic

todo

No Weakening

See Monotonicity of Entailment.

In classical logic, if you know $A$ is true, you can infer that $A\wedge A$ is true (contraction, idempotent), and you can also use $A$ as many times as you want. If you can prove $B$ from $A$, and you know $A$, then $B$ is true, and $A$ remains available. Similarly, if you have proved $B$, you can infer $A⟹B$ even if $A$ wasn’t used (weakening).

Linear logic operates differently: Every hypothesis (premise) must be used exactly once in a derivation. You cannot simply ignore a resource.