Mix

From LLWiki
Jump to: navigation, search

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

Binary \rulename{Mix} rule


\AxRule{\vdash\Gamma}
\AxRule{\vdash\Delta}
\LabelRule{Mix_2}
\BinRule{\vdash\Gamma,\Delta}
\DisplayProof

The \rulename{Mix_2} rule is equivalent to \bot\vdash\one:


\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

They are also equivalent to the principle A\tens B \vdash A\parr B:


\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

Nullary \rulename{Mix} rule


\LabelRule{Mix_0}
\NulRule{\vdash}
\DisplayProof

The \rulename{Mix_0} rule is equivalent to \one\vdash\bot:


\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

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


\AxRule{\vdash\Gamma}
\LabelRule{Mix_0}
\NulRule{\vdash}
\LabelRule{Mix_2}
\BinRule{\vdash\Gamma}
\DisplayProof

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

Personal tools