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

For logicians and computer scientists, it extends classical modal logic results to constructive settings, providing foundational tools for reasoning about constructive modal logics.

This paper develops a categorical duality for constructive modal logic CK, linking algebraic and birelational semantics, and uses it to prove Sahlqvist-style correspondence and completeness results, as well as a Goldblatt-Thomason-style definability theorem.