Multiplicative Conjunction (Linear Logic)

linear-logic

Definition

Multiplicative Conjunction ( Linear Logic)

$A\otimes B$ means “have $A$ and $B$ together, each exactly once”. Using $A\otimes B$ consumes one $A$ and one $B$ to proceed. No copying, no discarding.

The operator bundles independent resources. In a proof / program, building $A\otimes B$ means you can produce $A$ and $B$ from disjoint portions of your context.

Analogy: To create a pancake, both $Flour$ and $Egg$ are needed. Denote this “bundle” as:

$$Flour\otimes Egg\cong Flour\otimes Egg$$

The multiplicative conjunction $\otimes$ forms a monoid $⟨M,\otimes ⟩$ with a neutral elementi $1$, i.e.:

$$\forall A\in M:1\otimes A\cong A\cong A\otimes 1$$

Sequent Rules

Right (introduce $\otimes$): split resources to build each side

$$\frac{\Gamma ⊢A\Delta ⊢B}{\Gamma ,\Delta ⊢A\otimes B}(\otimes R)$$

Left (use $\otimes$): to use a bundle, open it

$$\frac{\Gamma ,A,B⊢C}{\Gamma ,A\otimes B⊢C}(\otimes L)$$