Two-dimensional Kripke Semantics II: Stability and Completeness
G. A. Kavvos
TL;DR
The paper addresses a mismatch between Kripke and algebraic semantics for intuitionistic and intuitionistic modal logic, proposing stable semantics with distributive-lattice worlds to achieve equi-completeness with the algebraic view. It then categorifies these ideas to two-dimensional stable semantics, establishing a 2-duality with categories of product-preserving presheaves in the style of Lawvere theories. The modal extension uses stable bimodules to model adjoint modalities, proving soundness and completeness, and yielding a duality on morphisms that aligns stable and algebraic perspectives. Finally, it develops a two-dimensional, category-theoretic account for both intuitionistic and modal logics, employing Sind completions, Day convolution, and stable profunctors to connect to coherent frames and algebraic theories, with potential links to choice-free dualities and higher-algebraic structures.
Abstract
We revisit the duality between Kripke and algebraic semantics of intuitionistic and intuitionistic modal logic. We find that there is a certain mismatch between the two semantics, which means that not all algebraic models can be embedded into a Kripke model. This leads to an alternative proposal for a relational semantics, the stable semantics. Instead of an arbitrary partial order, the stable semantics requires a distributive lattice of worlds. We constructively show that the stable semantics is exactly as complete as the algebraic semantics. Categorifying these results leads to a 2-duality between two-dimensional stable semantics and categories of product-preserving presheaves, i.e. models of algebraic theories in the style of Lawvere.