Lewis meets Brouwer: Constructive strict implication

LoCo Advancedweek 1 each day

Tadeusz Litak (University of Erlangen-Nuremberg)
Albert Visser (Utrecht University)

Website: https://www8.cs.fau.de/people/dr-tadeusz-litak/esslli-2021-lectures/

Abstract: 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".