We carry out a semantic study of the constructive modal logic CK. We provide a categorical duality linking the algebraic and birelational semantics of the logic. We then use this to prove Sahlqvist style correspondence and completeness results, as well as a Goldblatt-Thomason style theorem on definability of classes of frames.

翻译：我们对构造性模态逻辑CK进行了语义学研究。我们建立了一种范畴对偶性，将逻辑的代数语义与双关系语义联系起来。随后利用这一对偶性证明了Sahlqvist式的对应性与完备性定理，以及关于框架类可定义性的Goldblatt-Thomason式定理。