RanaldCloustonApr 24

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

IMLA 26

RanaldCloustonAug 2, 2024
I am excited to announce a new (submitted preprint) paper, on intuitionistic #modalLogic (s) and their Kripke frames (relational semantics). If interested please do read the paper, which is co-written with Jim de Groot and Ian Shillito, but I'll also write a short thread here about it too... https://arxiv.org/abs/2408.00262 #logic #intuitionisticLogic
Semantical Analysis of Intuitionistic Modal Logics between CK and IK

The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments, with only some remaining conservative over the standard axiomatisation of intuitionistic modal logic with necessity (box) alone. We show that relational Kripke semantics for CK can be extended with frame conditions for all axioms in the standard axiomatisation of IK, as well as other axioms previously studied. This allows us to answer open questions about the (non-)conservativity of such logics over intuitionistic modal logic without diamond. Our results are formalised using the Coq Proof Assistant.

arXiv.org
jaredAug 28, 2023

Even in our most idle wanderings, we don’t wander very far from home.

Reading Keisler “Elementary Calculus” a few weeks ago, I revisited John Bell’s paper “An Invitation to Smooth Infinitesimal Analysis”, which in turn prompted me to order Bell’s short book, “A Primer of Infinitesimal Analysis”.

I didn’t expect such a heavy dose of #CategoryTheory in this book! I might finally learn that topic seriously.

The fascinating treatment by JL Bell also touches upon another idle interest of mine: #IntuitionisticLogic . I’ve also been curious about systems that omit the excluded middle or well-ordering, etc., but I had never really looked at practical usages for such logics.

A fun, fresh look at #calculus all around

Leonardo PachecoDec 20, 2022

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