Multiplicative Disjunction (Linear Logic)

linear-logic

Definition

Multiplicative Disjunction ( Linear Logic)

$A⅋B$ is the multiplicative disjunction, the dual of $A\otimes B$.

Intuition: a consumer-style connective - ready to interact with whichever of $A$ or $B$ the context supplies. No implicit copying or discarding.

In an intuitionistic (single-succedent) presentation it is standard to define par by duality:

$$A⅋B:=(A^{\perp }\otimes B^{\perp }{)}^{\perp }.$$

Analogy: A universal socket that can accept either plug type the environment offers; once one is provided, the interaction continues and resources are consumed.

Algebraic laws. Associative/commutative with neutral element $\perp$:

$$A⅋\perp \cong A\cong \perp ⅋A$$

Duality: $(A⅋B{)}^{\perp }\cong A^{\perp }\otimes B^{\perp }$.

Sequent Rules

Intuitionistic (via definition).
Since $A⅋B$ is defined as $(A^{\perp }\otimes B^{\perp }{)}^{\perp }$, its use/intro rules are inherited from those of $\otimes$ and linear negation. Typical readings:

• Right (introduce $⅋$): to show $\Gamma ⊢A⅋B$, it suffices to show $\Gamma ,A^{\perp },B^{\perp }⊢\perp$ (i.e., derive absurdity from accepting either counter-resource).
• Left (use $⅋$): having $\Gamma ,A⅋B$ behaves like having a consumer that will proceed once the context supplies one of $A$ or $B$; operationally, you pattern-match by providing either $A$ or $B$ and continue.

Classical (multi-succedent) presentation (for reference).

• Right (introduce $⅋$): $$\frac{\Gamma ⊢\Delta ,A,B}{\Gamma ⊢\Delta ,A⅋B}(⅋R)$$
• Left (use $⅋$): $$\frac{\Gamma ,A⊢\Delta \Gamma ,B⊢\Delta }{\Gamma ,A⅋B⊢\Delta }(⅋L)$$

Contrast with $\otimes$.
$\otimes$ bundles independent productions you already have; $⅋$ is its dual, waiting to consume whichever of $A$ or $B$ the context can provide.