Logic and Computation Courses

Advanced Courses

Lewis meets Brouwer: Constructive strict implication

Tadeusz Litak and Albert Visser

Week 1, August 3-7, 2020


C. I. Lewis invented modern modal logic as a theory of "strict implication". Over the classical propositional calculus one can as well work with the unary box connective. Intuitionistically, however, the strict implication has greater expressive power and allows distinctions invisible in the ordinary syntax. Thus, in this course we study constructive systems of strict implication. We discuss conditions to be imposed on Kripke semantics, axiomatization of the minimal system and some of its extensions, and some basic correspondence results.

We illustrate
- when and how this logic collapses to that of unary box;
- how classical assumptions made the trivialization of Lewis original 1918 system inevitable.

Furthermore, we present two interpretations of this system. The first comes from provability logic, more specifically preservativity in extensions of Heyting's Arithmetic. The second, Curry-Howard one is provided by functional programming: the study of Haskell "arrows" as contrasted with "idioms" or "applicative functors".


Connect with us

32nd European Summer School in Logic, Language and Information - ESSLLI 2021
Please send any queries to

  • esslli@uu.nl