Timeline for Linear logic with storage preserving positives
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 3, 2022 at 20:50 | comment | added | Lê Thành Dũng 'Tito' Nguyễn | 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$). | |
| Nov 29, 2017 at 10:14 | comment | added | Damiano Mazza | 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! | |
| Nov 28, 2017 at 14:50 | comment | added | Mike Shulman | 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. | |
| Nov 28, 2017 at 14:27 | comment | added | Mike Shulman | @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. | |
| Nov 28, 2017 at 10:23 | comment | added | Andrej Bauer | 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. | |
| Nov 28, 2017 at 6:02 | history | asked | Mike Shulman | CC BY-SA 3.0 |