Lewis meets Brouwer, or perhaps Heyting

Abstract: This talk is an introduction to what one might call the Heyting-Lewis calculus of strict implication over the intuitionistic propositional base; the names "constructive strict implication" or "Brouwer-Lewis implication/calculus" have also been used. The corresponding class of algebras can be seen as the fusion of Heyting algebras and weak Heyting algebras (Celani and Jansana) over the shared bounded lattice reduct. (Super)intuitionistic modal logics with unary box are a limiting case, but in the intuitionistic setting there are many examples where strict implication is not reducible to box. Its variants arise, e.g., in the context of preservativity in Heyting Arithmetic (where it was first invented by Visser), in the inhabitation logic of simple type theory extended with Haskell-style arrows, and in a generalization of Intuitionistic Epistemic Logic of Artemov and Protopopescu. The move to the intuitionistic propositional base also throws interesting light on the complex fate of Lewis' original systems. The Heyting-Lewis calculus enjoys a natural Kripke semantics (first studied by Iemhoff and coauthors), which also allows defining an appropriate notion of descriptive frame and Esakia-style dualities. Furthermore, one can follow the Wolter-Zakharyaschev idea of generalizing the Gödel-McKinsey-Tarski translation, reducing the metatheory of Heyting-Lewis logics to suitable bimodal logics over the classical propositional base, obtaining a suitable variant of the Blok-Esakia theorem, and (re)proving many correspondence, completeness, decidability and fmp results in an uniform way. However, it seems that ultimately one will have to drop one of the axioms, losing the natural Kripke semantics. In the final part of the talk, I am going to discuss alternative semantics for the weakened system and its position in the broader landscape of intuitionistic logics with an additional implication-like connective. This talk involves joint work with Albert Visser (Utrecht University), Jim de Groot and Dirk Pattinson (ANU), Igor Sedlar and the Prague group, and Miriam Polzer (Google).

logic

Audience: researchers in the topic

Nonclassical Logic Webinar