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.

翻译：我们重新审视直觉主义逻辑与直觉主义模态逻辑的克里普克语义与代数语义之间的对偶关系。我们发现这两种语义之间存在某种不匹配，这意味着并非所有代数模型都能嵌入到克里普克模型中。这引出了对关系语义的一种替代方案——稳定语义。稳定语义不要求任意的偏序结构，而要求世界构成一个分配格。我们通过构造性方法证明，稳定语义的完备性与代数语义完全一致。将这些结果进行范畴化，可得到二维稳定语义与保积预层范畴（即劳维尔风格的代数理论模型）之间的2-对偶关系。