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.
翻译:本文为带有$\Box$算子的直觉主义模态逻辑提出了一种新的余代数语义。特别地,我们基于图像有限偏序集,给出了直觉主义描述模态框架与直觉主义模态克里普克框架的余代数表示。这为这些框架类在余代数逻辑领域中的一个问题提供了解决方案,该问题已由Litak(2014)以及de Groot与Pattinson(2020)明确提出。我们的关键技术工具是Ghilardi构造的一个近期推广,其形式为Esakia空间范畴到Priestley空间范畴的包含函子的右伴随。作为这些结果的应用,我们研究了直觉主义模态框架的双模拟,描述了自由模态Heyting代数的对偶空间,并为余代数直觉主义逻辑理论的建立提供了一条路径。