http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Mix&feed=atom&action=history
Mix - Revision history
2024-03-29T02:22:13Z
Revision history for this page on the wiki
MediaWiki 1.19.20+dfsg-0+deb7u3
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Mix&diff=590&oldid=prev
Olivier Laurent: Definition and main properties of the mix rules
2013-10-27T13:59:24Z
<p>Definition and main properties of the mix rules</p>
<p><b>New page</b></p><div>The usual notion of <math>\rulename{Mix}</math> is the binary version of the rule but a nullary version also exists.<br />
<br />
== Binary <math>\rulename{Mix}</math> rule ==<br />
<br />
<math><br />
\AxRule{\vdash\Gamma}<br />
\AxRule{\vdash\Delta}<br />
\LabelRule{Mix_2}<br />
\BinRule{\vdash\Gamma,\Delta}<br />
\DisplayProof<br />
</math><br />
<br />
The <math>\rulename{Mix_2}</math> rule is equivalent to <math>\bot\vdash\one</math>:<br />
<br />
<math><br />
\LabelRule{\one}<br />
\NulRule{\vdash\one}<br />
\LabelRule{\one}<br />
\NulRule{\vdash\one}<br />
\LabelRule{Mix_2}<br />
\BinRule{\vdash\one,\one}<br />
\DisplayProof<br />
\qquad<br />
\AxRule{\vdash\Gamma}<br />
\LabelRule{\bot}<br />
\UnaRule{\vdash\Gamma,\bot}<br />
\AxRule{\vdash\one,\one}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\vdash\Gamma,\one}<br />
\AxRule{\vdash\Delta}<br />
\LabelRule{\bot}<br />
\UnaRule{\vdash\Delta,\bot}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\vdash\Gamma,\Delta}<br />
\DisplayProof<br />
</math><br />
<br />
They are also equivalent to the principle <math>A\tens B \vdash A\parr B</math>:<br />
<br />
<math><br />
\LabelRule{\one}<br />
\NulRule{\vdash\one}<br />
\LabelRule{\one}<br />
\NulRule{\vdash\one}<br />
\LabelRule{\tens}<br />
\BinRule{\vdash\one\tens\one}<br />
\AxRule{\vdash\bot\parr\bot,\one\parr\one}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\vdash\one\parr\one}<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\vdash\bot,\one}<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\vdash\bot,\one}<br />
\LabelRule{\tens}<br />
\BinRule{\vdash\bot\tens\bot,\one,\one}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\vdash\one,\one}<br />
\DisplayProof<br />
\qquad<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\vdash A\orth,A}<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\vdash B\orth,B}<br />
\LabelRule{Mix_2}<br />
\BinRule{\vdash A\orth,A,B\orth,B}<br />
\LabelRule{\parr}<br />
\UnaRule{\vdash A\orth,B\orth,A\parr B}<br />
\LabelRule{\parr}<br />
\UnaRule{\vdash A\orth\parr B\orth,A\parr B}<br />
\DisplayProof<br />
</math><br />
<br />
== Nullary <math>\rulename{Mix}</math> rule ==<br />
<br />
<math><br />
\LabelRule{Mix_0}<br />
\NulRule{\vdash}<br />
\DisplayProof<br />
</math><br />
<br />
The <math>\rulename{Mix_0}</math> rule is equivalent to <math>\one\vdash\bot</math>:<br />
<br />
<math><br />
\LabelRule{Mix_0}<br />
\NulRule{\vdash}<br />
\LabelRule{\bot}<br />
\UnaRule{\vdash\bot}<br />
\LabelRule{\bot}<br />
\UnaRule{\vdash\bot,\bot}<br />
\DisplayProof<br />
\qquad<br />
\LabelRule{\one}<br />
\NulRule{\vdash\one}<br />
\AxRule{\vdash\bot,\bot}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\vdash\bot}<br />
\LabelRule{\one}<br />
\NulRule{\vdash\one}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\vdash}<br />
\DisplayProof<br />
</math><br />
<br />
The nullary <math>\rulename{Mix}</math> acts as a unit for the binary one:<br />
<br />
<math><br />
\AxRule{\vdash\Gamma}<br />
\LabelRule{Mix_0}<br />
\NulRule{\vdash}<br />
\LabelRule{Mix_2}<br />
\BinRule{\vdash\Gamma}<br />
\DisplayProof<br />
</math><br />
<br />
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.</div>
Olivier Laurent