Stable Canonical Rules for Intuitionistic Modal Logics
Cheng Liao
TL;DR
This work develops a uniform, algebraic–geometric method of stable canonical rules for intuitionistic modal logics, showing that every intuitionistic modal multi-conclusion consequence relation is axiomatizable by such rules. It provides an alternative, self-contained proof of the Blok–Esakia theorem in this setting and extends the correspondence to multi-conclusion logics via Gödel translations and dualities with bimodal logics. A Dummett–Lemmon-style completeness result is established for the intuitionistic modal multi-conclusion framework, again leveraging stable canonical rules and the Blok–Esakia machinery. The approach relies on stable embeddings, the closed domain condition, and a rich network of dualities (Priestley/Esakia/ modal Esakia spaces) to translate syntactic properties into finite, refutable patterns, with significant implications for decidability and Kripke completeness in these logics.
Abstract
This paper develops stable canonical rules for intuitionistic modal logics, which were first introduced for superintuitionistic logics and transitive nor mal modal logics in [1] and [2] respectively. We first prove that every in tuitionistic modal multi-conclusion consequence relation is axiomatizable by stable canonical rules. This allows us to assume, without loss of generality, that rules considered by us are stable canonical ones. The idea turns out to be useful. In particular, using stable canonical rules, we get an alterna tive proof of the Blok-Esakia theorem for intuitionistic modal logics which was first proved in [3] and generalize it to multi-conclusion consequence re lations. We also prove the Dummett-Lemmon conjecture for intuitionistic modal multi-conclusion consequence relations, which, as far as we know, is a new result.