Tomorrow belongs to deviant intuitionistic modalities

• Tadeusz Litak
• Department Informatik, Technische Fakultät, FAU Erlangen-Nürnberg, Germany

Abstract: Intuitionistic modal logics are an immensely vast area, rediscovered each decade since at least 1940's with varying motivations. However, it seems fair to say that traditionally trained logicians focused their attention mostly on those which arise by picking some standard modal axiom (K, S4, T etc.) and replacing classical propositional basis with IPC. In this informal talk, I would like to focus on a few prominent logics, whose axioms would classically yield very trivial beasts, as their sound classical Kripke frames can only be (disjoint unions of) singleton points.

The minimal member of the whole family - its "greatest common denominator" - can be adequately described in the programming lingo as the logic of "applicative functors" of McBride-Patterson or in the categorical lingo, the logic of pointed (and product-preserving) endofunctors. Its extensions include Propositional Lax Logic (PLL), which can be described in programming lingo as the Curry-Howard counterpart of Moggi's "computational metalanguage" or in the categorical lingo as the logic of (strong) monads. Another extension of interest includes "strong Loeb logic", which reappears in type systems for guarded (co-recursion) since the seminal work of Nakano fifteen years ago; its categorical semantics is systematically investigated by Stefan Milius and myself, but specific examples (like ultrametric spaces) are well-known and often used. Finally, there is also the modalized Heyting Calculus (mHC) investigated by Tbilisi and Moscow schools since 1970's; I'm presently working on its computational meaning in terms of constructive control operators. So far, mHC managed to fly entirely under the radar of the programming community, but its axioms happen to be valid in almost all models of step-indexing or guarded (co-)recursion proposed in the recent literature.

Proof systems for the base system and its extensions appear both more elegant and more usable as "programming languages" than those for general modal logics. As another example of improvements in the metatheory, I can mention my ongoing work on negative translations in intuitionistic modal logic. As it turns out, for the logic in this family, the Kuroda translation is always adequate, whereas there are extensions of intuitionistic K for which even the Kolmogorov translation fails.

If time allows, I can also discuss some by-products of my ongoing collaboration with Albert Visser on elimination of fixpoints and uniform interpolation in intuitionistic Loeb logics. Our work indicates, in particular, that it may be preferable to adopt as the primitive connective Lewis' original strict implication. Interestingly, in the intuitionistic setting, this connective is no longer definable using unimodal box.