Multiplicative Disjunction (Linear Logic)

Definition

Multiplicative Disjunction ( Linear Logic)

$⅋$ is the multiplicative disjunction, the dual of .

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

In an intuitionistic (single-succedent) presentation it is standard to define par by duality:
$⅋$
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 :
$⅋ ⅋$
Duality: $⅋$ .

Sequent Rules

Intuitionistic (via definition).
Since $⅋$ is defined as , its use/intro rules are inherited from those of and linear negation. Typical readings:

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

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

Right (introduce $⅋$ ): $⅋ ⅋$
Left (use $⅋$ ): $⅋ ⅋$

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

Lukas' Notes

Multiplicative Disjunction (Linear Logic)

Table of Contents

Definition

Sequent Rules