ESSLLI 2021 lectures

Lewis meets Brouwer: Constructive strict implication

ESSLLI 2020 (postponed to 2021) advanced course. Area: Logic and Computation

Lecturers: Tadeusz Litak and Albert Visser
Provisional schedule
  • Day 1 (Litak): Motivation, history, axiomatization and algebraic semantics. The classical problems of Lewis. Curry-Howard correspondence, Hughes’ arrows, monads and idioms in functional programming. Towards Intuitionistic Logic of Entailments?
    Main reference: Litak and Visser, Lewis meets Brouwer: constructive strict implication
    Slides (handout version)
  • Day 2 (Litak):  Kripke semantics for “sharp” HLC (i.e., in the presence of axiom Di). Completeness and correspondence results via a Gödel-McKinsey-Tarski translation into a suitable bimodal classical logic: explicit or extrinsic perspective (van Benthem terminology).
    Main reference: de Groot, Litak, Pattinson, Gödel-McKinsey-Tarski and Blok-Esakia for Heyting-Lewis Implication 
    Slides
  • Day 3/Day 4 (Visser): Arithmetical Interpretations: Löb meets Heyting
    Slides (updated after the course)
  • Day 4, part II (Litak) What holds in the absence of Di? Algebraic semantics of “flat” HLC. Countermodel search using tools such as Mace4  versus the use of SQEMA in the sharp case.
    Slides
  • Day 5 (Visser): The Case of the Missing Fixed Point Calculation
    Slides (updated after the course)

Main reference for the second half of the course: Litak and Visser, Lewisian Fixed Points I: Two Incomparable Constructions

Additional reading

Please see a very detailed list in our original ESSLLI proposal.

Even more additional reading

There are some references not included in our proposal, which I mentioned in the Slack channel while answering students’ questions: