# Linear logic with storage preserving positives

Has anyone studied a version of linear logic in which the storage modality $!$ preserves the positive connectives and quantifiers $\otimes,\oplus,\exists$? That is, such that we have $!(A\otimes B) = !A \otimes !B$ and $!(A\oplus B) = !A \oplus !B$ and $!\exists x. A = \exists x.!A$. It seems that there ought to be a reasonable sequent calculus for such a theory, e.g. using a "modal context zone" as in Girard's LU or Pfenning's LV enhanced with left rules that allow introducing $\otimes,\oplus,\exists$ in the modal zone.

• That looks weird. Naively speaking, if you have $!(A \otimes B)$ you can produce any number of pairs $(a, b)$ so you will have the same amount of $A$'s and $B$'s. But with $!A \otimes !B$ you can have some number of $A$'s and some other number of $B$'s. – Andrej Bauer Nov 28 '17 at 10:23
• @AndrejBauer Well, actually I'm mainly interested in affine logic with this property, so that you could forget some of the $A$'s or the $B$'s. – Mike Shulman Nov 28 '17 at 14:27
• But in general, yes, these are additional assumptions, not implied by the ordinary meaning of $!$. Categorically speaking, they just say that a certain comonad is monoidal and cocontinuous, which doesn't seem unreasonable. – Mike Shulman Nov 28 '17 at 14:50
• I don't think anyone has ever considered such a variant of linear logic. For provability, maybe you don't even need "modal zones", it should be enough to consider modified sequent calculus rules like $$\frac{\Gamma,!^nA,!^nB\vdash C}{\Gamma,!^n(A\otimes B)\vdash C}$$ (with $!^n$ meaning $!\cdots !$ $n$ times, $n$ arbitrary) and similarly for $\oplus$ and $\exists$. But this breaks cut-elimination... Making cut-elimination work seems much less trivial and may involve enhanced "modal zones" like you say, but I don't see how. By the way, good question! – Damiano Mazza Nov 29 '17 at 10:14