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

Additive Disjunction

Definition

Additive Disjunction ( Linear Logic)

$A\oplus B$ means the provider makes an internal choice: it commits to either $A$ or $B$ and proceeds on that branch (the other branch is discarded). No implicit copying or discarding beyond the chosen branch.

In a proof / program, constructing $A\oplus B$ means you present either a proof of $A$ (left injection) or a proof of $B$ (right injection), tagged accordingly.

Analogy: A notification bot chooses its channel:

$$\text{Notify}:=\mathrm{SMS}\oplus \mathrm{Email}$$

The additive disjunction $\oplus$ is associative/commutative with neutral element $0$:

$$A\oplus 0\cong A\cong 0\oplus A$$

Duality: $(A\oplus B{)}^{\perp }\cong A^{\perp }\&B^{\perp }$.

Link to original

Additive Conjunction

Definition

Additive Conjunction ( Linear Logic)

$A\&B$ (read “with”) means the environment makes an external choice: it may demand either $A$ or $B$, and the provider must be ready to handle the chosen branch. Only the chosen branch continues.

In a proof / program, constructing $A\&B$ means you can produce $A$ and (with the same context) produce $B$; offering $A\&B$ promises readiness for either.

Analogy: A service menu:

$$\text{Beverage}:=\mathrm{Tea}\&\mathrm{Coffee}$$

The additive conjunction $\&$ is associative/commutative with neutral element $\top$:

$$A\&\top \cong A\cong \top \&A$$

Duality: $(A\&B{)}^{\perp }\cong A^{\perp }\oplus B^{\perp }$.

Link to original

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.