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.
Henry Story (Apr 08 2020 at 18:08):Hi, I am constantly swimming between Philosophy and Category Theory (and programming)
Over the last year ½ I have slowly come to discover via Abramsky 1993 Game Semantics (for which he gives a Category of Games), and then found pursuing this view that the view of logic as dialogical has got a huge amount of wind behind it. I read parts of Brandom 10 years ago, but I can now see how much influence he has had on logic. Here are some really interesting things I discovered recently
Anyway it would be interesting to have views here if anyone has come across work in CT that goes in this direction, or goes against it.
Finished the excellent "Immanent Reasoning or Equality in Action". Great insights in §10 §11 into the dialogical philosophy of type theory. Has there been more work on the material interpretation of CTT @lamiradj @NicolasClerbout? https://link.springer.com/book/10.1007%2F978-3-319-91149-6 https://twitter.com/bblfish/status/1243650652963815424/photo/1
- The 🐟 BabelFish (@bblfish)
Henry Story (Apr 09 2020 at 18:49):Reading "Meaning in Dialogue" I came across the dual logic to intutionistic logic "falsification logic" which this 2005 article argues fits the process of scientific research better https://twitter.com/bblfish/status/1248243867490672641
It looks at Intutionistic Logic from the point of view of a Kripke semantics. If so both should be understandable coalgebraically since "Modal Logics are coalgebraic".
So here's an intriguing thesis: Where Intuitionistic Logic best describes Mathematical truths, it's dual, "falsification Logic" may be better adapted to scientific research. https://link.springer.com/article/10.1007/s11225-005-8474-7 https://twitter.com/bblfish/status/1248243867490672641/photo/1
- The 🐟 BabelFish (@bblfish)
John Baez (Apr 09 2020 at 18:52):The dual to intuitionistic logic is often called "paraconsistent logic" or "Brazilian logic" - those terms are good for finding references.
John Baez (Apr 09 2020 at 18:53):I think @Mike Shulman has written about a logic that combines intuitionistic or "verification" logic and paraconsisent or "falsification" logic.
John Baez (Apr 09 2020 at 18:55):Well, now I think maybe I'm mischaracterizing what he did. But it's here:
John Baez (Apr 09 2020 at 18:55):https://golem.ph.utexas.edu/category/2018/05/linear_logic_for_constructive.html
Henry Story (Apr 09 2020 at 18:56):yep, that article says Falsification logic is a type of paraconsistent logic.
The view of scientific research there is certainly idealized, but the duality of those is very intriguing.
Henry Story (Apr 09 2020 at 19:35):Trafford in Meaning in Dialogue p93-94 then argues that this does not fit Lakatos' view of scientific progress, and goes on to look at a more symmetrical logic more appropriate for dialogue which he calls "bi-intuitionistic logic"
Henry Story (Apr 09 2020 at 19:52):Re.linear logic, I have an idea in the back of my head that it is particularly appropriate for dealing with speech acts. (since many acts are unique. Eg. buying something is a unique act. buying it twice would get one two items not one.)
John Baez (Apr 09 2020 at 20:44):@Henry Story - I gave you a mistaken link to the discussion here on Bi-Heyting algebra. The link I'm giving you now is the correct one.
The incorrect link took you to a private UCR discussion group, and I'm gonna kick you out of that now. Sorry - my fault. There's a lot more about Bi-Heyting algebras here.
Gershom (Apr 09 2020 at 21:12):a lovely work on linear logic as verification and refutation (which is a more purely-logical predecessor to shulman's stuff) is noamz's phd dissertation: http://noamz.org/thesis.pdf
Henry Story (Apr 09 2020 at 21:25):Did part of the conversation above just dissappear?
The part about the relation of linear logic to game semantics and session types?
Someone reminded me of session types, which I had started looking at a month or so ago. The Wadler article Propositions as Sessions was recommended. And I pointed to the 2019 talk "Two sides of the same Coin: Session Types and Game Semantics" recorded here https://www.youtube.com/watch?v=px38U3jsOLQ
John Baez (Apr 09 2020 at 21:30):Someone may have moved the stuff about session types here: Session types.
Maybe they decided this wasn't "Philosophy" and deserved its own thread.
Henry Story (Apr 09 2020 at 21:34):Ah, I see. There should be a duplication button, rather than a move button. Or at least a link, as it's a bit confusing. :-)
I thought it is quite neat how one can start off reading about protocols, find out about session types, go to linear logic, find out a vast literature on dialogical logic (from a philosophical point of view), and end up back at session types as linear logic and game semantics. :upside_down:
James Wood (Apr 09 2020 at 21:40):Ah sorry, I didn't want to cause too much disruption of the topic, so I split it off. Now we have the classic problem that this conversation should also be split off...
Henry Story (Apr 09 2020 at 21:54):unless there is a way to tie this into Girard's Ludics, which seems to be about how conversations need only not diverge. :smile:
Mohamar Rios (Apr 09 2020 at 22:18):I remember reading Popper's paper on falsifiability and very much feeling like falsifiability described a logic somehow dual to the Intuitionistic logic but I had no idea it had been formalized. That's totally awesome!
John Baez (Apr 09 2020 at 22:29):By the way, you get a model of verifiability logic (intuitionistic logic) by looking at the Heyting algebra of open sets in a topological space, the intuition being that if you know something for sure it should remain true under small perturbations. You get some models of falsifiability logic by looking at the co-Heyting algebra of closed sets in a topological space. There should be some story about all this, measurements in physics, and also measure theory, which often involves the sigma-algebra of Borel sets in a topological space, which is a Boolean algebra (and thus both a Heyting algebra and co-Heyting algebra).
Christian Williams (Apr 09 2020 at 23:40):We have a stream for #philosophy.