Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The cut rule for linear logic used to be stated as
If $\Gamma \vdash A$ and $A \vdash \Delta$, then $\Gamma \vdash \Delta$.
I don’t think this is general enough, so I corrected it to
If $\Gamma \vdash A, \Phi$ and $\Psi,A \vdash \Delta$, then $\Psi,\Gamma \vdash \Delta,\Phi$.
No objection, but I guess it would depend on the precise rules. In MLL which has duals, if we have rules which allow us to derive
$\frac{\Gamma \vdash \Sigma,\Phi}{\Gamma, \Phi^\ast \vdash \Sigma}, \qquad \frac{\Psi, \Sigma \vdash \Delta}{\Psi \vdash \Delta, \Sigma^\ast}$where $\Phi^\ast$ is the list of duals of formulas of $\Phi$, and $A^{\ast\ast} = A$, I thought we would be able to derive your more general cut rule from the more specific cut rule:
$\array{ \arrayopts{\rowlines{solid}} \Gamma \vdash A, \Phi\;\;\;\;\;\;\;\;\; \Psi, A \vdash \Delta \\ \Gamma, \Phi^\ast \vdash A \;\;\;\;\;\;\;\;\; A \vdash \Psi^\ast, \Delta \\ \Gamma, \Phi^\ast \vdash \Psi^\ast, \Delta \\ \Psi, \Gamma \vdash \Delta, \Phi }$Yes, you’re right. But I think it’s better to formulate the rule in a way that remains correct in fragments without involutive negation.
Understood (and agreed); I was just explaining the likely reason the original form was the way it was (I’m guessing I wrote that).
1 to 13 of 13