My paper 'Semantical Analysis of Intuitionistic Modal Logics between CK and IK', with Jim de Groot and Ian Shillito, is now in its final edited preprint form: https://arxiv.org/abs/2408.00262 . I will travelling to #LICS #LICS2025 to present it in Singapore in late June. #logic #modalLogic
#ModalLogic
$Trump ordered government agencies to prepare for mining the ocean floor.
Just because it is legal does not mean you should do it. Permission is not obligation.
Just say no. They have no power if you ignore them.
I’m in Amsterdam, about to give a talk about proof theory for modal predicate logic at the ILLC, the home base of the modal industrial complex. I have no idea how this is going to go over, but it should be a fun ride, however it turns out.
With the NWO XL consortium on Cyclic Structures in Programs and Proofs, we are looking for 6 highly motivated and talented PhD students starting in September (with some flexibility).
The topics range from Modal logic, proof theory, and coalgebras to Programming languages, concurrency, and type systems and Proof assistants (#Agda, #Rocq).
Information about the positions and application procedure can be found on the website:
cyclic-structures.gitlab.io/vacancies/
Applications will be evaluated on a rolling basis but should be submitted by the 23rd of May for full consideration.
Please forward to any strong candidates you know!
#TypeTheory #ModalLogic #Concurrency #ProgrammingLanguages #TypeSystems #ProofAssistants #CyclicStructures #PhD #Netherlands #UniversityOfGroningen #LeidenUniversity #UniversityOfTwente #TUDelft #RadboudUniversity
The topics range from Modal logic, proof theory, and coalgebras to Programming languages, concurrency, and type systems and Proof assistants (#Agda, #Rocq).
Information about the positions and application procedure can be found on the website:
cyclic-structures.gitlab.io/vacancies/
Applications will be evaluated on a rolling basis but should be submitted by the 23rd of May for full consideration.
Please forward to any strong candidates you know!
#TypeTheory #ModalLogic #Concurrency #ProgrammingLanguages #TypeSystems #ProofAssistants #CyclicStructures #PhD #Netherlands #UniversityOfGroningen #LeidenUniversity #UniversityOfTwente #TUDelft #RadboudUniversity
I'm glad to have space to get to writing, and the first writing project of my sabbatical has reached first-draft stage. If you're interested in modal logic, proof theory, and the metaphysics of contingent existence, have I got the paper for you!
https://consequently.org/writing/mlce-ge2/
I've got to say, I think the hypersequent calculus in this paper is pretty neat.
A short note I wrote a few months ago just got published: https://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/2293-06.pdf
I show that diamonds are already embedded in Artemov and Protopopescu's intuitionistic epistemic logic (they are just double negations).
This is part of some work I'm doing to understand diamonds in intuitionistic modal logics.
It’s a cloudy and cold Tuesday, and I’m inside writing about refinement.
At least I *think* I understand what I’m doing a bit better than Mark S and his team of macrodata refiners do.
(That’s an inappropriate #Severance, #prooftheory #ModalLogic and #ClickyKeyboard crossover post. I’m sorry about that.)
The lower order comes up unexpectedly (to me) in coevolutionary algorithms (what I studied in my PhD), but really in search and optimization more broadly.
Say you have a notion of "context", and a way of ordering these so that some contexts are larger, more expansive than, or "above" others. And let's say in each context, there is a set of things that are identifiable as "best". I'm being vague because you can instantiate this basic idea pretty broadly. For instance, maybe the contexts are states of information in a search algorithm and "best" refers to the possible solutions that seem best in each state of information; as you search, you change (increase) your state of information, and might change your might about which possible solutions are the best one. As another example, the contexts could be possible worlds and "best" refers to which propositions are true in each possible world; as you progress from one possible world to the next, you might change your mind about what propositions are true.
Anyway, with that simple setup you can associate to each thing the set of all contexts in which it appears best. This set could be empty or could be very large or anything in between. Then the lower order shows up as a weak preference relationship among all the things: one thing is lower preference than another if, for each context in which it appears best, there's a larger or equal context in which the other thing seems best. Put differently, any time you think the first thing is best, there's a way to increase your context such that the other thing appears best. This is exactly the lower order between the sets of contexts in which each thing seems best. If the set of contexts in which one thing seems best is higher up the lower order (😝) than the set of contexts in which the other seems best, then the former thing is weakly preferred to the latter.
The intuition in a search setting is that contexts are states of information, a kind of compendium of what you've learned so far in your search. If x and y are possible solutions, and for every context (state of information) in which you think x is the best there is always a bigger context--i.e., with more information--in which you think y is best instead, you ought to prefer y to x. The rationale is that any time you think x is best there's a way to learn a little more and change your mind to think y is best instead, which justifies preferring y to x.
Applied to modal logic, this notion corresponds to validity: if in every possible world where the proposition p is true there is an accessible world in which proposition q is true, then "p implies possibly q" is true in every world (valid).
The appearance of "possibly" is suggestive I think, and concords with this being a weak preference. "Necessarily" would be a strong preference, but I'd expect (in the sense of demand) a search process follow such a preference directly.
#math #ComputerScience #search #CoevolutionaryAlgorithm #SolutionConcept #ModalLogic
Say you have a notion of "context", and a way of ordering these so that some contexts are larger, more expansive than, or "above" others. And let's say in each context, there is a set of things that are identifiable as "best". I'm being vague because you can instantiate this basic idea pretty broadly. For instance, maybe the contexts are states of information in a search algorithm and "best" refers to the possible solutions that seem best in each state of information; as you search, you change (increase) your state of information, and might change your might about which possible solutions are the best one. As another example, the contexts could be possible worlds and "best" refers to which propositions are true in each possible world; as you progress from one possible world to the next, you might change your mind about what propositions are true.
Anyway, with that simple setup you can associate to each thing the set of all contexts in which it appears best. This set could be empty or could be very large or anything in between. Then the lower order shows up as a weak preference relationship among all the things: one thing is lower preference than another if, for each context in which it appears best, there's a larger or equal context in which the other thing seems best. Put differently, any time you think the first thing is best, there's a way to increase your context such that the other thing appears best. This is exactly the lower order between the sets of contexts in which each thing seems best. If the set of contexts in which one thing seems best is higher up the lower order (😝) than the set of contexts in which the other seems best, then the former thing is weakly preferred to the latter.
The intuition in a search setting is that contexts are states of information, a kind of compendium of what you've learned so far in your search. If x and y are possible solutions, and for every context (state of information) in which you think x is the best there is always a bigger context--i.e., with more information--in which you think y is best instead, you ought to prefer y to x. The rationale is that any time you think x is best there's a way to learn a little more and change your mind to think y is best instead, which justifies preferring y to x.
Applied to modal logic, this notion corresponds to validity: if in every possible world where the proposition p is true there is an accessible world in which proposition q is true, then "p implies possibly q" is true in every world (valid).
The appearance of "possibly" is suggestive I think, and concords with this being a weak preference. "Necessarily" would be a strong preference, but I'd expect (in the sense of demand) a search process follow such a preference directly.
#math #ComputerScience #search #CoevolutionaryAlgorithm #SolutionConcept #ModalLogic
Et pourquoi les modèles de Kripke n'auraient pas un ensemble de mondes possibles finis? Pour parler d'un système comme les états d'un programme, ça paraît raisonnable.
The Nordic Logic Summer School is now in full swing here in Reykjavík. I’ve given my first proof theory class, and Rineke Verbrugge is introducing modal logic and social cognition.
Today's #blog looks at a general, albeit oddly controversial, recipe for generating sequent calculi from possible worlds https://blogs.fediscience.org/the-updated-scholar/2024/05/24/discussing-proof-analysis-in-modal-logic/ #logic #modalLogic
Today's #blog , delayed a few weeks as I waited for a physical copy of the book, looks at the (or maybe 'a'?) standard textbook on #ModalLogic https://blogs.fediscience.org/the-updated-scholar/2024/04/23/discussing-modal-logic/ #logic
An explanation of what axioms and mathematical proofs really are. With a reference to my tool that helps exploring some of them.
https://math.codidact.com/posts/290943/291261#answer-291261
#Logic #Axioms #Mathematics #ProofTheory #HilbertSystems #ModalLogic #Research #Software
Today's #blog is about a fascinating recent development in our understanding - or perhaps exposure of our lack of understanding - of intuitionistic #modalLogic https://blogs.fediscience.org/the-updated-scholar/2024/04/05/discussing-on-intuitionistic-diamonds-and-lack-thereof/ #logic
I've had a lot of fun this week combing through some old intuitionistic #ModalLogic papers for my #blog . Does anyone know anything, other than what is in her papers, about the career of the logician Gisèle Fischer Servi? https://blogs.fediscience.org/the-updated-scholar/2024/03/22/discussing-on-modal-logic-with-an-intuitionistic-base/ #logic #WomenInLogic
On my #blog today we discuss how Moggi's calculus of #monads can be seen as a #ModalLogic https://blogs.fediscience.org/the-updated-scholar/2024/02/27/discussing-computational-types-from-a-logical-perspective/ #logic
What is the difference between a Kripke frame and a frame skeleton in modal logic?
A new preprint of our (Rance Cleaveland, Peter Fontana and yt) work regarding timed mu-calculi: https://arxiv.org/abs/2310.04100 (not accepted for publication yet).
We present the first timed mu-calculus that is more expressive than timed CTL for arbitrary timed automata.
Client Info
Server: https://mastodon.social
Version: 2025.04
Repository: https://github.com/cyevgeniy/lmst