In linear logic sequent calculus, can $\Gamma \vdash \Delta$ and $\Sigma \vdash \Pi$ be combined to get $\Gamma, \Sigma \vdash \Delta, \Pi$?

Question

Linear logic is a certain variant of sequent calculus that does not generally allow contraction and weakening. Sequent calculus does admit the cut rule: given contexts $\Gamma$, $\Sigma$, $\Delta$, and $\Pi$, and a proposition $A$, we can make the inference

$$\frac{\Gamma \vdash A, \Delta \qquad \Sigma, A \vdash \Pi}{\Gamma, \Sigma \vdash \Delta, \Pi}.$$

So what I'm wondering is if it's also possible to derive a "cut rule with no $A$":

$$\frac{\Gamma \vdash \Delta \qquad \Sigma \vdash \Pi}{\Gamma, \Sigma \vdash \Delta, \Pi}.$$

Answer 1

The rule you suggest is called the "mix" rule , and it is not derivable from the standard rules of linear logic. Actually, what I know is that it's not derivable in multiplicative linear logic; I can't imagine that additive or exponential rules would matter, but I don't actually know that they don't. Hyland and Ong constructed a game semantics for multiplicative linear logic that violates the mix rule.