#modallogic — Public Fediverse posts

The deadline for submission of abstracts to #IMLA (Intuitionistic Modal Logic and Applications) has been extended to 30 April. It would be great if I were to see some of you there (at least, at the banquet for that weekend's #FLoC workshops).

"Constructive and intuitionistic modal logics, and their connections with type theory and computation, remain foundationally and practically significant in computer science, logic, and related areas. These include applications in type disciplines, meta-logics for computational phenomena, and explanatory frameworks in philosophical logic. The workshop aims to explore theoretical and methodological issues at the intersection of constructive proof theory and modal semantics, as well as practical questions about which modal connectives and rules best capture computational phenomena at appropriate levels of abstraction."

**Invited speakers**
- Danel Ahman (University of Tartu, Estonia)
- Brigitte Pientka (McGill University, Montreal, Canada)
- Ranald Clouston (ANU, Canberra, Australia)
- More to be confirmed

https://sonia-marin.github.io/imla26/

#ModalLogic #IntuitionisticLogic #Logic

8th Workshop on Intuitionistic Modal Logic and Applications (IMLA)
24–25 July 2026, Lisbon, Portugal
Affiliated with the Federated Logic Conference (FLoC 26)
https://sonia-marin.github.io/imla26/

Constructive and intuitionistic modal logics, and their connections with type theory and computation, remain foundationally and practically significant in computer science, logic, and related areas. These include applications in type disciplines, meta-logics for computational phenomena, and explanatory frameworks in philosophical logic. The workshop aims to explore theoretical and methodological issues at the intersection of constructive proof theory and modal semantics, as well as practical questions about which modal connectives and rules best capture computational phenomena at appropriate levels of abstraction.

**Invited speakers**
- Brigitte Pientka (McGill University, Montreal, Canada)
- Ranald Clouston (ANU, Canberra, Australia)
- More to be confirmed.

**Submissions**
We invite abstracts for contributed talks of up to *2 pages* (excluding bibliography). They may describe published work, unpublished work, or work in progress. We especially encourage submissions from students and early-career researchers.

Abstracts should be submitted via the workshop’s submission page:
https://submissions.floc26.org/imla/

(ctd)

#Logic #ModalLogic #CallForAbstracts

New preprint! https://arxiv.org/abs/2601.03762 . This is our 2nd paper on the intuitionistic modal logic CK and its extensions. We look at 'duality', the relationship between Kripke semantics and universal algebra. There are various dualities in the literature, but ours has some unusual features, including our 'exploding world' which satisfies all formula, including contradictions! Dualities allow results in algebra to be ported to the modal world, as we do in the 2nd half of the paper to, for example, give a description of which classes of possible worlds can be axiomatically defined. #Logic #ModalLogic

In this week's #blog I write briefly about a 2001 paper on designing lambda calculi for intuitionistic modal logic. https://blogs.fediscience.org/the-updated-scholar/2025/08/15/discussing-extended-curry-howard-correspondence-for-a-basic-constructive-modal-logic/ #logic #modalLogic #proofTheory #typeTheory

New preprint: Functional Causation Beyond Spacetime: A Non-Metric Framework for Temporal Structure

Can causal direction emerge from internal asymmetries rather than geometry?

📄 PDF: https://philpapers.org/rec/LENFCB
🔍 #Causality #ModalLogic #StructuralRealism #PhilosophyOfPhysics

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

$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.

#JustSayNo #ModalLogic #RM3

$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.

#JustSayNo #ModalLogic #RM3

$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.

#JustSayNo #ModalLogic #RM3

$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.

#JustSayNo #ModalLogic #RM3

$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.

#JustSayNo #ModalLogic #RM3

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.

https://consequently.org/presentation/2025/mlce-illc/

#prooftheory #modalLogic

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.

#ProofTheory #ModalLogic #Metaphysics

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.

#Logic #ModalLogic

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.)

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.)

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.)

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.)

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 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.

https://consequently.org/class/2024/nls-proof-theory/

#ProofTheory #ModalLogic

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

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

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

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

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

Note to self:

\(\Box\) — L — konieczność
\(\Diamond\) — M — możliwość

#ModalLogic #Logic

What is the difference between a Kripke frame and a frame skeleton in modal logic?

#logic #ModalLogic

#statistics #linguistics #semantics #ModalLogic #logic

https://www.gov.uk/government/news/defence-intelligence-communicating-probability

@linguistics

Next week on my #blog I'll write something about a quite recent paper, the 2020 'Multimodal Dependent Type Theory' https://dl.acm.org/doi/10.1145/3373718.3394736 #TypeTheory #ModalLogic

In this week's #blog I talk about a paper I know very well, Davies and Pfenning's 'A Modal Analysis of Staged Computation' https://updatedscholar.blogspot.com/2023/02/discussing-modal-analysis-of-staged.html #ModalLogic #CurryHoward

In this week's #blog I talk about a paper I know very well, Davies and Pfenning's 'A Modal Analysis of Staged Computation' https://updatedscholar.blogspot.com/2023/02/discussing-modal-analysis-of-staged.html #ModalLogic #CurryHoward

Later this week, or maybe next week, on my #blog I'll be writing about Davies and Pfenning's 'A Modal Analysis of Staged Computation' https://dl.acm.org/doi/abs/10.1145/382780.382785 #Logic #ModalLogic

Advancing automated theorem proving for the modal logics D and S5. ~ Jens Otten. https://ceur-ws.org/Vol-3326/ARQNL2022_paper5.pdf #ATP #ModalLogic #MleanCoP #nanoCoPM

I find 𝐾𝑃→𝑃 a quite reasonable axiom for epistemic logic. In an intuitive sense, one cannot know something false, that’s not knowing. But i find the dual 𝑃→𝐾̂𝑃 not satisfying. I’ve seen explanations of the dual modality 𝐾̂ as “epistemic possibility”; but I don’t think truth does not implies epistemic possibility.

#Logic #ModalLogic #EpistemicLogic

I find 𝐾𝑃→𝑃 a quite reasonable axiom for epistemic logic. In an intuitive sense, one cannot know something false, that’s not knowing. But i find the dual 𝑃→𝐾̂𝑃 not satisfying. I’ve seen explanations of the dual modality 𝐾̂ as “epistemic possibility”; but I don’t think truth does not implies epistemic possibility.

#Logic #ModalLogic #EpistemicLogic

I find 𝐾𝑃→𝑃 a quite reasonable axiom for epistemic logic. In an intuitive sense, one cannot know something false, that’s not knowing. But i find the dual 𝑃→𝐾̂𝑃 not satisfying. I’ve seen explanations of the dual modality 𝐾̂ as “epistemic possibility”; but I don’t think truth does not implies epistemic possibility.

#Logic #ModalLogic #EpistemicLogic

I find 𝐾𝑃→𝑃 a quite reasonable axiom for epistemic logic. In an intuitive sense, one cannot know something false, that’s not knowing. But i find the dual 𝑃→𝐾̂𝑃 not satisfying. I’ve seen explanations of the dual modality 𝐾̂ as “epistemic possibility”; but I don’t think truth does not implies epistemic possibility.

#Logic #ModalLogic #EpistemicLogic

Yesterday, I did a presentation on fixed-points in IS5, an intuitionistic variation of the modal logic S5.
Slides available here: https://leonardopacheco.xyz/slides/akiu-2022.pdf

#Logic #ModalLogic #IntuitionisticLogic

Let’s ask ChatGPT the truly serious questions, starting off with some quantified modal logic and the necessitism/contingentism debate.

(Unsurprisingly, it sounds like an undergraduate who has some sense of what the words mean but hasn't done the work and is doing a bad job of word association and looking up Wikipedia summaries.)

#PhilLogic #ModalLogic #ChatGPT