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$
$\endgroup$
5
asked Nov 28, 2017 at 6:02
-
$\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 BauerCommented Nov 28, 2017 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 ShulmanCommented Nov 28, 2017 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 ShulmanCommented Nov 28, 2017 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 MazzaCommented Nov 29, 2017 at 10:14
-
$\begingroup$ One thing this reminds me of is Olivier Laurent's polarized linear logic, where weakening and contraction are allowed on any positive formula ($!A$ being considered positive for any $A$). $\endgroup$– Lê Thành Dũng 'Tito' NguyễnCommented Nov 3, 2022 at 20:50
Add a comment
|