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.
Recent searches
Search options
#ModalLogic
0 posts0 participants0 posts today
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
Cyclic Structures in Programs and ProofsVacancies
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.)
Continued thread
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
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.
math.codidact.comWhat is the significance of the K-axiom in modal logic S5?In normal modal logic S5, the K axiom says $\square (p \rightarrow q) \rightarrow (\square p \rightarrow \square q)$.
First of all, is this an abuse...
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
Note to self:
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.
arXiv.orgExpressiveness Results for Timed Modal Mu-CalculiThis paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (real) time with a general framework for defining formulas recursively; several variants have been proposed in the literature. We show that one logic, which we call $L^{rel}_{ν,μ}$, is strictly more expressive than the other mu-calculi considered. It is also more expressive than the temporal logic TCTL, while the other mu-calculi are incomparable with TCTL in the setting of general timed automata.
Did you know that some people will refuse a slice of cake if you don’t give them a chance to eat the whole cake?
Also, did you know that there is no point in driving anywhere if you can’t travel at the speed of light?
#ModalLogic #Capitalism #IncomeCap
contd
Here is what I consider one of the biggest
mistakes of all in #modallogic: concentration on a system with just one
modal operator. The only way to have any philosophically significant re-
sults in deontic logic or epistemic logic is to combine those operators with:
tense operators (otherwise how can you formulate principles of change?);
the logical operators (otherwise how can you compare the relative with
the absolute?); the operators like historical or physical necessity (otherwise
how can you relate the agent to his environment?); and so on and so on.
But where to stop? This list can be extended further and further. One
must stop somewhere, but to stop the list at one is obviously missing out
on something important. The point I am trying to make is that the
semantics being explained here allows for several operators side by side
in a simple convenient. and natural way: one has only to think what
coordinates i = (w, t, p. a . ... ) one wants. Furthermore one should not
forget the logical operators.