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

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.

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

Last revised on September 8, 2018 at 23:28:10. See the history of this page for a list of all contributions to it.