nLab mix rule

Definition

The mix rule is an inference rule that can be added to linear logic. The most common mix rule is the binary mix rule

$$\frac{\Gamma \vdash \Delta \quad \Gamma' \vdash \Delta'} {\Gamma, \Gamma' \vdash \Delta, \Delta'}$$

(or $\Gamma \otimes \Gamma' \vdash \Delta \parr \Delta'$), but to be unbiased one should also consider the nullary mix rule

$$\frac{} {\vdash}$$

(or $\mathbf{1} \vdash \bot$), which together are equivalent to $\mathbf{1} \equiv \bot$, and imply $n$-ary mix rules for all $n$.

Semantics

Ordinary linear logic has semantics in polycategories, linearly distributive categories, and star-autonomous categories, depending on how many connectives are assumed. A linearly distributive category satisfies the binary mix rule if there is a morphism $\bot \to \mathbf{1}$ satisfying a certain coherence axiom. It additionally satisfies the nullary mix rule if this morphism is an isomorphism. In CS97 these are called mix categories and isomix categories respectively.

References

• Robin Cockett and R.A.G. Seely, 1997. Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. 1997. TAC 5:3. Web.