You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Paolo Perrone (Jul 01 2020 at 20:40):Hello all! This is the thread of discussion for the talk of Brendan Fong, David J. Myers and David I. Spivak, "Behavioral Mereology: A Modal Logic for Passing Constraints".
Date and time: Thursday July 9, 20:40 UTC.
Zoom meeting: https://mit.zoom.us/j/7488874897
YouTube live stream: https://www.youtube.com/watch?v=F9Yxw_PlDfY&list=PLCOXjXDLt3pZDHGYOIqtg1m1lLOURjl1Q
Paolo Perrone (Jul 09 2020 at 19:44):Please notice the new Zoom address!
Paolo Perrone (Jul 09 2020 at 20:30):(10 minutes!)
Paolo Perrone (Jul 09 2020 at 21:00):Here's the paper: https://arxiv.org/abs/1811.00420
Paolo Perrone (Jul 09 2020 at 21:01):Blog post mentioned: https://golem.ph.utexas.edu/category/2019/06/behavioral_mereology.html
Georgios Bakirtzis (Jul 09 2020 at 21:10):I saw the question about requirements interoperability and I am wondering if you guys are aware of the work in engineering using linear temporal logic
Georgios Bakirtzis (Jul 09 2020 at 21:10):and how your approach might generalize that work or otherwise assist it
Valeria de Paiva (Jul 09 2020 at 22:26):hi @David Jaz I simply meant that usually over an intuitionistic basis we consider 2 accessibility relations, a $$\leq$ and an R as in this very old paper Categorical and Kripke Semantics for Constructive S4 Modal Logic (with Natasha Alechina and Michael Mendler and Eike Ritter). In Proc. of Computer Science Logic (CSL'01), LNCS 2142, ed L. Fribourg. 2001 https://link.springer.com/chapter/10.1007/3-540-44802-0_21
or if you prefer a not so old paper https://arxiv.org/pdf/1605.08106.pdf
Valeria de Paiva (Jul 09 2020 at 22:46):thinking a bit more since the talk, I do understand @Tarmo Uustalu suggestion, but I don't think like v. much the approach. When you go for labelled systems like Alex's, which indeed form a nice framework in geometric logic, you lose some of the properties that made you want to do Curry-Howard for modal logic to begin with. In particular I think to this day we don't have a proof of decidability of IS4. (though I may be wrong as I last thought about it in 2005?). the point is that constructive modal logics are a bit of a open-ended project, as we don't know exactly the theorems we think should be true. We know (as Alex points out) a collection of requirements on the set of theorems, they shouldn't make diamonds defined in terms of boxes, the system should be conservative over the basis, we hope to have existence and disjunction properties, etc but a fundamental question is whether diamonds should distribute over disjunctions or not. Prawitz' system does not satisfy it, the Simpson system does.
David Jaz (Jul 09 2020 at 23:07):Thanks Valeria! I'll take a look at these references.
Our diamond and box are not interdefineable (unless one assumes LEM), but as a left adjoint our diamond does commute with disjunction (and existential quantification).
So the takeaway might be that it isn't right for us to say that our modalities generalize constructive S4 modal logic without wading into the difficult question of what precisely is constructive modal logic, or what should it be?
Valeria de Paiva (Jul 10 2020 at 00:12):David Jaz said:
Thanks Valeria! I'll take a look at these references.
Our diamond and box are not interdefineable (unless one assumes LEM), but as a left adjoint our diamond does commute with disjunction (and existential quantification).
So the takeaway might be that it isn't right for us to say that our modalities generalize constructive S4 modal logic without wading into the difficult question of what precisely is constructive modal logic, or what should it be?
Yes, you've got to be at least a little careful, as usually an equivalence relation as the modal accessibility relation implies S5, not S4. if it's an S4 system then you need to choose between IS4 (Simpson's thesis 1994) or CS4 (Prawitz 1965, Natural Deduction book, chapter 6). Simpson system satisfies distribution of diamond over disjunction, Prawitz CS4 does not. these are facts in propositional modal logic, if you're doing your calculations over a topos (higher-order logic) maybe the calculations need to be adjusted, I believe in this case a new proof might be required, but I don't know much. (glad to see that I found the right place to write this in!)
Paolo Perrone (Jul 10 2020 at 02:15):Video here!
https://www.youtube.com/watch?v=vERL6UWgcJs&list=PLCOXjXDLt3pYot9VNdLlZqGajHyZUywdI
Valeria de Paiva (Jul 10 2020 at 03:36):Giorgos Bakirtzis said:
I saw the question about requirements interoperability and I am wondering if you guys are aware of the work in engineering using linear temporal logic
Sorry, I missed this before. I am not aware of the work in engineering using linear temporal logic. do you want to post a reference, please? thanks!
Georgios Bakirtzis (Jul 10 2020 at 05:42):Fainekos and the general pappas control theory group introduced it https://repository.upenn.edu/cgi/viewcontent.cgi?article=1061&=&context=grasp_papers&=&sei-redir=1&referer=https%253A%252F%252Fscholar.google.com%252Fscholar%253Fq%253Dlinear%252Btemporal%252Blogic%252Bfainekos%2526hl%253Den%2526as_sdt%253D0%2526as_vis%253D1%2526oi%253Dscholart#search=%22linear%20temporal%20logic%20fainekos%22
Georgios Bakirtzis (Jul 10 2020 at 05:42):It’s pretty much used all the time now
Georgios Bakirtzis (Jul 10 2020 at 05:43):Paulo tabuada also has some work I think and recently Miroslav pajic
Valeria de Paiva (Jul 10 2020 at 05:51):Many thanks! "linear" here seems to be like in "linear temporal logic LTL,CTL, not as in Girard's Linear Logic.
Georgios Bakirtzis (Jul 10 2020 at 13:27):Yeah sorry that wasn't clear. For what it is worth, I thought I could innovate in this field (LTL, CTL specifications) with linear logic some 4 years ago before even knowing categories but failed at learning linear logic :P So I think there is something here