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.

  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Nov 28 '17 at 10:23
  • $\begingroup$ @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. $\endgroup$ – Mike Shulman Nov 28 '17 at 14:27
  • $\begingroup$ 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. $\endgroup$ – Mike Shulman Nov 28 '17 at 14:50
  • $\begingroup$ 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! $\endgroup$ – Damiano Mazza Nov 29 '17 at 10:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.