Two-dimensional Kripke Semantics I: Presheaves
G. A. Kavvos
TL;DR
The paper addresses the challenge of unifying Kripke-style relational semantics with categorical semantics for intuitionistic modalities. It develops a two-dimensional, proof-relevant Kripke framework using bimodules and Kan extensions to generate adjoint modalities $\blacklozenge$ and $\Box$, and then categorifies to presheaf categories to obtain a canonical, proof-relevant semantics via $\FUNC{\CC}{\SET}$. Extending further to profunctors, it shows how endoprofunctors yield a robust two-dimensional Kripke semantics for modal logic, with precise dualities between relational frames and categorical models (e.g., $\EBIMOD^{op}_{cc,moo}\simeq \PRIMEALGLATTO_{\Rightarrow o}$ and $\EPROF^{op}_{cc,moo}\simeq \PSHCATO_{\Rightarrow o}$). The work establishes that presheaf categories categorify prime algebraic lattices, and that open, modal-open, and rs (retraction-surjectivity) conditions translate across these dualities, providing a cohesive, high-level framework for intuitionistic modal logic and its type-theoretic interpretations. Overall, the approach offers a unified semantic foundation that supports synthetic reasoning with modalities across logic, category theory, and computer science.
Abstract
The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.