The mix rule

The 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.