Modal Intuitionistic Logics as Dialgebraic Logics

Duality is one of the key techniques in the categorical treatment of modal logics. From the duality between (modal) algebras and (descriptive) frames one derives e.g. completeness (via a syntactic characterisation of algebras) or definability (using a suitable version of the Goldblatt-Thomason theorem). This is by now well understood for classical modal logics and modal logics based on distributive lattices, via extensions of Stone and Priestley duality, respectively. What is conspicuously absent is a comprehensive treatment of modal intuitionistic logic. This is the gap we are closing in this paper. Our main conceptual insight is that modal intuitionistic logics do not appear as algebra/coalgebra dualities, but instead arise naturally as dialgebras. Our technical contribution is the development of dualities for dialgebras, together with their logics, that instantiate to large class of modal intuitionistic logics and their frames as special cases. We derive completeness and expressiveness results in this general case. For modal intuitionistic logic, this systematises the existing treatment in the literature.

• Theory of computation → Modal and temporal logics.