Additive Disjunction (Linear Logic)

linear-logic

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 }$.

Sequent Rules

Right sequent (introduce $\oplus$): commit to one branch

$$\frac{\Gamma ⊢A}{\Gamma ⊢A\oplus B}(\oplus R_1)\frac{\Gamma ⊢B}{\Gamma ⊢A\oplus B}(\oplus R_2)$$

Left sequent (use $\oplus$): case analysis (be ready for either)

$$\frac{\Gamma ,A⊢C\Gamma ,B⊢C}{\Gamma ,A\oplus B⊢C}(\oplus L)$$