nLab mix rule

The mix rule

The mix rule


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 1\mathbf{1} \vdash \bot), which together are equivalent to 1\mathbf{1} \equiv \bot, and imply nn-ary mix rules for all nn.


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


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