Mix Rule

A binary mix rule is an Inference Rule that can be added to a Sequent Calculus, which states that

$\par\frac{\Gamma_{1}\vdash\Delta_{1}\qquad\Gamma_{2}\vdash\Delta_{2}}{\Gamma_{% 1},\Gamma_{2}\vdash\Delta_{1},\Delta_{2}}$

There is also a nullary nullary mix rule, which states that

$\par\frac{}{\cdot\vdash\cdot}$

When taken together, binary and nullary mix rules along with the rule

A\vdash A

give n-ary mix rules:

$\par\frac{}{\Gamma\vdash\Gamma}$

Examples

In the Classical Sequent Calculus, the binary mix rule is not very controversial; this is essentially the statement that $A\land B\vdash A\lor B$ . However, the nullary mix rule is very obviously inconsistent, as it says that $\top\vdash\bot$ !
If we transform a Natural Deduction calculus into a sequent calculus by looking at its calculus of Simultaneous Substitutions, then the n-ary mix rule comes from the fact that we have identity substitutions. From a logical perspective, this is akin to using formal Conjunctions on both sides of the sequent.
Every category with Finite Biproducts validates the nary mix rule when using products on the left and coproducts on the right. Maps between biproducts are a lot like Matrices, so the resulting sequent calculus acts like a logic of matrices.
Every Normal Duoidal Category validates the nullary mix rule.