A Coalgebraic Semantics for Intuitionistic Modal Logic

TL;DR

This paper introduces a new coalgebraic semantics for intuitionistic modal logic with the ox operator, providing algebraic representations of frames and Kripke models based on image-finite posets, addressing open problems in coalgebraic logic.

Contribution

It offers a novel coalgebraic framework for intuitionistic modal logic, including representations of frames and dual spaces, advancing the theoretical understanding of coalgebraic semantics.

Findings

Provides algebraic representations of intuitionistic modal frames

Describes dual spaces of free modal Heyting algebras

Advances coalgebraic theory for intuitionistic modal logic

Abstract

We give a new coalgebraic semantics for intuitionistic modal logic with $\Box$. In particular, we provide a colagebraic representation of intuitionistic descriptive modal frames and of intuitonistic modal Kripke frames based on image-finite posets. This gives a solution to a problem in the area of coalgebaic logic for these classes of frames, raised explicitly by Litak (2014) and de Groot and Pattinson (2020). Our key technical tool is a recent generalization of a construction by Ghilardi, in the form of a right adjoint to the inclusion of the category of Esakia spaces in the category of Priestley spaces. As an application of these results, we study bisimulations of intuitionistic modal frames, describe dual spaces of free modal Heyting algebras, and provide a path towards a theory of coalgebraic intuitionistic logics.