Linear Logic

logic

Definition

Linear Logic

todo

Operators

Multiplicative Conjunction

Definition

Multiplicative Conjunction ( Linear Logic)

$A\otimes B$ means “have $A$ and $B$ together, each exactly once”. Using $A\otimes B$ consumes one $A$ and one $B$ to proceed. No copying, no discarding.

The operator bundles independent resources. In a proof / program, building $A\otimes B$ means you can produce $A$ and $B$ from disjoint portions of your context.

Analogy: To create a pancake, both $Flour$ and $Egg$ are needed. Denote this “bundle” as:

$$Flour\otimes Egg\cong Flour\otimes Egg$$

The multiplicative conjunction $\otimes$ forms a monoid $⟨M,\otimes ⟩$ with a neutral elementi $1$, i.e.:

$$\forall A\in M:1\otimes A\cong A\cong A\otimes 1$$

Link to original

Symbols

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. From $\Gamma ⊢C$, inferring $\Gamma ,A⊢C$ is not allowed.