Two-dimensional Kripke Semantics II: Stability and Completeness

TL;DR

This paper introduces the stable semantics as an alternative to traditional Kripke semantics for intuitionistic modal logic, establishing its completeness and categorical duality with algebraic models.

Contribution

It proposes the stable semantics with a distributive lattice of worlds and proves its completeness and duality with algebraic models, addressing a mismatch in existing semantics.

Findings

Stable semantics is as complete as algebraic semantics.

A 2-duality between stable semantics and categories of product-preserving presheaves.

Constructive proof of the equivalence between stable and algebraic semantics.

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.