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.

othernumber of $B$'s. $\endgroup$ – Andrej Bauer Nov 28 '17 at 10:23affinelogic with this property, so that you could forget some of the $A$'s or the $B$'s. $\endgroup$ – Mike Shulman Nov 28 '17 at 14:27additionalassumptions, 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. $\endgroup$ – Mike Shulman Nov 28 '17 at 14:50