Additive Conjunction (Linear Logic)

linear-logic

Definition

Additive Conjunction ( Linear Logic)

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

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

Analogy: A service menu:

The additive conjunction is associative/commutative with neutral element :

Duality: .

Sequent Rules

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

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