Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Coalgebraic Semantics for Intuitionistic Modal Logic

Rodrigo Nicolau Almeida, Nick Bezhanishvili

TL;DR

The paper addresses the problem of providing a coalgebraic semantics for intuitionistic modal logic with $\Box$, focusing on descriptive intuitionistic modal frames and image-finite Kripke frames. It introduces the $V_{G}$ and $V^{\uparrow}$ constructions and proves equivalences: $\mathbf{CoAlg}(V_{G}(V^{\uparrow}(-))) \simeq \mathbf{DiG}$ and $\mathbf{CoAlg}(P_{G}(\mathsf{Up}(-))) \simeq \mathbf{ImFinK}$, thereby enabling a modular coalgebraic treatment of intuitionistic frames. The paper also provides a bisimulation correspondence, a dual description of the free modal Heyting algebra on finitely many generators, and a pathway to coalgebraic intuitionistic logic via neighbourhood-style semantics. Together, these results create a framework for extending coalgebraic methods to intuitionistic logics and suggest avenues for handling logics such as $\mathsf{S4}$ in a coalgebraic setting.

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.

A Coalgebraic Semantics for Intuitionistic Modal Logic

TL;DR

The paper addresses the problem of providing a coalgebraic semantics for intuitionistic modal logic with , focusing on descriptive intuitionistic modal frames and image-finite Kripke frames. It introduces the and constructions and proves equivalences: and , thereby enabling a modular coalgebraic treatment of intuitionistic frames. The paper also provides a bisimulation correspondence, a dual description of the free modal Heyting algebra on finitely many generators, and a pathway to coalgebraic intuitionistic logic via neighbourhood-style semantics. Together, these results create a framework for extending coalgebraic methods to intuitionistic logics and suggest avenues for handling logics such as in a coalgebraic setting.

Abstract

We give a new coalgebraic semantics for intuitionistic modal logic with . 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.
Paper Structure (15 sections, 19 theorems, 37 equations, 4 figures)

This paper contains 15 sections, 19 theorems, 37 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Duality Theory and Coalgebra
  4. Intuitionistic Modal Logic
  5. Descriptive general frames for IML
  6. Generalizing Ghilardi
  7. The functor $V_{G}$
  8. The functor $P_{G}$
  9. Main Results
  10. Applications
  11. Bisimulations of $\Box$-frames
  12. Constructing the Free Intuitionistic Modal algebra
  13. Coalgebraic Intuitionistic Logic
  14. Conclusions and Future Work
  15. Acknowledgements

Key Result

proposition 1

The assignment $V$ as above defines an endofunctor on $\mathbf{Stone}$. Moreover, for each $X$ a Stone space, the categories $\mathbf{CoAlg}(V)$ and $\mathbf{DG}$ are equivalent.

Figures (4)

  • Figure 1: Coalgebra morphism compatibility
  • Figure 2: Commuting Triangle of Priestley spaces
  • Figure 3: Bisimulations for the $P_{G}$
  • Figure 4: Intuitionistic Lifting of functor F

Theorems & Definitions (45)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • proposition 1
  • definition 7
  • proposition 2
  • definition 8
  • ...and 35 more