Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason

TL;DR

This paper explores the semantic foundations of constructive modal logic CK, establishing a duality between algebraic and birelational semantics, and deriving key correspondence, completeness, and definability results.

Contribution

It introduces a categorical duality for CK, enabling new correspondence and completeness theorems, and extends Goldblatt-Thomason style results to this logic.

Findings

Established a categorical duality linking algebraic and birelational semantics.

Proved Sahlqvist style correspondence and completeness results for CK.

Derived a Goldblatt-Thomason style theorem on class definability.

Abstract

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.