Additive Disjunction (Linear Logic)

linear-logic

Definition

Additive Disjunction ( Linear Logic)

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

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

Analogy: A notification bot chooses its channel:

The additive disjunction is associative/commutative with neutral element :

Duality: .

Sequent Rules

Right sequent (introduce ): commit to one branch

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