Olivier Laurent: Definition and main properties of the mix rules

2013-10-27T13:59:24Z

Definition and main properties of the mix rules

New page

The usual notion of <math>\rulename{Mix}</math> is the binary version of the rule but a nullary version also exists.

== Binary <math>\rulename{Mix}</math> rule ==

<math>
\AxRule{\vdash\Gamma}
\AxRule{\vdash\Delta}
\LabelRule{Mix_2}
\BinRule{\vdash\Gamma,\Delta}
\DisplayProof
</math>

The <math>\rulename{Mix_2}</math> rule is equivalent to <math>\bot\vdash\one</math>:

<math>
\LabelRule{\one}
\NulRule{\vdash\one}
\LabelRule{\one}
\NulRule{\vdash\one}
\LabelRule{Mix_2}
\BinRule{\vdash\one,\one}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma}
\LabelRule{\bot}
\UnaRule{\vdash\Gamma,\bot}
\AxRule{\vdash\one,\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\Gamma,\one}
\AxRule{\vdash\Delta}
\LabelRule{\bot}
\UnaRule{\vdash\Delta,\bot}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\Gamma,\Delta}
\DisplayProof
</math>

They are also equivalent to the principle <math>A\tens B \vdash A\parr B</math>:

<math>
\LabelRule{\one}
\NulRule{\vdash\one}
\LabelRule{\one}
\NulRule{\vdash\one}
\LabelRule{\tens}
\BinRule{\vdash\one\tens\one}
\AxRule{\vdash\bot\parr\bot,\one\parr\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\one\parr\one}
\LabelRule{\rulename{ax}}
\NulRule{\vdash\bot,\one}
\LabelRule{\rulename{ax}}
\NulRule{\vdash\bot,\one}
\LabelRule{\tens}
\BinRule{\vdash\bot\tens\bot,\one,\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\one,\one}
\DisplayProof
\qquad
\LabelRule{\rulename{ax}}
\NulRule{\vdash A\orth,A}
\LabelRule{\rulename{ax}}
\NulRule{\vdash B\orth,B}
\LabelRule{Mix_2}
\BinRule{\vdash A\orth,A,B\orth,B}
\LabelRule{\parr}
\UnaRule{\vdash A\orth,B\orth,A\parr B}
\LabelRule{\parr}
\UnaRule{\vdash A\orth\parr B\orth,A\parr B}
\DisplayProof
</math>

== Nullary <math>\rulename{Mix}</math> rule ==

<math>
\LabelRule{Mix_0}
\NulRule{\vdash}
\DisplayProof
</math>

The <math>\rulename{Mix_0}</math> rule is equivalent to <math>\one\vdash\bot</math>:

<math>
\LabelRule{Mix_0}
\NulRule{\vdash}
\LabelRule{\bot}
\UnaRule{\vdash\bot}
\LabelRule{\bot}
\UnaRule{\vdash\bot,\bot}
\DisplayProof
\qquad
\LabelRule{\one}
\NulRule{\vdash\one}
\AxRule{\vdash\bot,\bot}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\bot}
\LabelRule{\one}
\NulRule{\vdash\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash}
\DisplayProof
</math>

The nullary <math>\rulename{Mix}</math> acts as a unit for the binary one:

<math>
\AxRule{\vdash\Gamma}
\LabelRule{Mix_0}
\NulRule{\vdash}
\LabelRule{Mix_2}
\BinRule{\vdash\Gamma}
\DisplayProof
</math>

If <math>\pi</math> is a proof which uses no <math>\bot</math> rule and no weakening rule, then (up to the simplification of the pattern <math>\rulename{Mix_0}/\rulename{Mix_2}</math> above into nothing) <math>\pi</math> is either reduced to a <math>\rulename{Mix_0}</math> rule or does not contain any <math>\rulename{Mix_0}</math> rule.

Mix - Revision history

Olivier Laurent: Definition and main properties of the mix rules