Olivier Laurent: Non admissibility

2013-10-28T20:24:46Z

Non admissibility

New page

The additive cut rule is:
<math>
\AxRule{\Gamma\vdash A,\Delta}
\AxRule{\Gamma,A\vdash\Delta}
\LabelRule{\rulename{cut\;add}}
\BinRule{\Gamma\vdash\Delta}
\DisplayProof
</math>

In contrary to what happens in classical logic, this rule is '''not''' admissible in linear logic.

The formula <math>\alpha\plus\alpha\orth</math> is not provable in linear logic, while it is derivable with the additive cut rule:

<math>
\NulRule{\alpha\vdash\alpha}
\UnaRule{\vdash\alpha,\alpha\orth}
\LabelRule{\plus_{R2}}
\UnaRule{\vdash\alpha,\alpha\plus\alpha\orth}
\NulRule{\alpha\vdash\alpha}
\LabelRule{\plus_{R1}}
\UnaRule{\alpha\vdash\alpha\plus\alpha\orth}
\LabelRule{\rulename{cut\;add}}
\BinRule{\vdash\alpha\plus\alpha\orth}
\DisplayProof
</math>

Additive cut rule - Revision history

Olivier Laurent: Non admissibility