Stone Coalgebras and Completeness for Coalgebraic Modal Logic

Coalgebras have been studied as a general approach to dynamic systems. Modal logic seems to be a natural choice for a specification language for coalgebras. Given an endofuntor T the problem is how to define a suitable modal logic for T-coalgebras. Following an approach by Pattinson we first define for an arbitrary endofunctor T:Set ---> Set a modal logic and briefly discuss (sufficient) conditions for that logic to be sound, complete and expressive. We then translate this approach to the case in which we are given a functor T:Stone ---> Stone where Stone denotes the category of Stone spaces. We now obtain a better understanding of the above mentioned results of Pattinson: First we show that any coalgebraic modal logic gives rise to a functor L:BA --> BA, such that the category of L-algebras provides us an algebraic semantics for the logic. It then turns out that Pattinson's above mentioned conditions for soundness, completeness and expressiveness of the logic are in fact equivalent to L being the Stone dual of the functor T.  

hosted by