Additive Conjunction (Linear Logic)

linear-logic

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

Sequent Rules

Right sequent (introduce $\&$): prove both branches using the same context

$$\frac{\Gamma ⊢A\Gamma ⊢B}{\Gamma ⊢A\&B}(\&R)$$

Left sequent (use $\&$): project a branch (be able to continue from either)

$$\frac{\Gamma ,A⊢C}{\Gamma ,A\&B⊢C}(\&L_1)\frac{\Gamma ,B⊢C}{\Gamma ,A\&B⊢C}(\&L_2)$$