Gödel-McKinsey-Tarski and Blok-Esakia for Heyting-Lewis Implication
Jim de Groot, Tadeusz Litak, Dirk Pattinson
TL;DR
This work develops a comprehensive theory for Heyting-Lewis logics with a binary strict implication $\sto$. It builds algebraic (Heyting-Lewis algebras) and relational (sto-frames) semantics and proves a categorical duality between them. A Gödel–McKinsey–Tarski-style embedding translates $\mathcal{L}_{\sto}$ into classical bimodal logic $\mathsf{S4K}$, enabling a Blok–Esakia-type theorem that links $\mathsf{iA}$-logics to their modal companions and yields canonicity, correspondence, the finite model property, and decidability for a broad family of logics. The results extend to descriptive frames and provide transfer principles that allow leveraging the rich classical modal theory to derive semantic and metatheoretic properties of intuitionistic logics with strict implication. Overall, the paper advances both the theory and the toolset for analyzing binary modal operators in intuitionistic settings, with potential applications to Curry–Howard correspondences, preservativity, and epistemic interpretations.
Abstract
Heyting-Lewis Logic is the extension of intuitionistic propositional logic with a strict implication connective that satisfies the constructive counterparts of axioms for strict implication provable in classical modal logics. Variants of this logic are surprisingly widespread: they appear as Curry-Howard correspondents of (simple type theory extended with) Haskell-style arrows, in preservativity logic of Heyting arithmetic, in the proof theory of guarded (co)recursion, and in the generalization of intuitionistic epistemic logic. Heyting-Lewis Logic can be interpreted in intuitionistic Kripke frames extended with a binary relation to account for strict implication. We use this semantics to define descriptive frames (generalisations of Esakia spaces), and establish a categorical duality between the algebraic interpretation and the frame semantics. We then adapt a transformation by Wolter and Zakharyaschev to translate Heyting-Lewis Logic to classical modal logic with two unary operators. This allows us to prove a Blok-Esakia theorem that we then use to obtain both known and new canonicity and correspondence theorems, and the finite model property and decidability for a large family of Heyting-Lewis logics.