Gödel-McKinsey-Tarski and (not quite) Blok-Esakia for Heyting-Lewis Implication

Jim de Groot, Tadeusz Litak, Dirk Pattinson

Heyting-Lewis Logic is the extension of intuitionistic propositional logic with a strict implication connective that satisfies the constructive counterparts of axioms for strict im…