Moss' logic for ordered coalgebras
share
We present a finitary coalgebraic logic for T-coalgebras, where T is a locally monotone endofunctor of the category of posets and monotone maps that preserves exact squares and finite intersections. The logic uses a single cover modality whose arity is given by the dual of the coalgebra functor T, and the semantics of the modality is given by relation lifting. For the finitary setting to work, we need to develop a notion of a base for subobjects of TX. This in particular allows us to talk about a finite poset of subformulas for a given formula, and of a finite poset of successors for a given state in a coalgebra. The notion of a base is introduced generally for a category equipped with a suitable factorisation system. We prove that the resulting logic has the Hennessy-Milner property for the notion of similarity based on the notion of relation lifting. We define a sequent proof system for the logic and prove its completeness.
READ FULL TEXT