(draft) … (up)
The idea of this section is to run through parts of [HK04] and adapt it to ordered neighbourhood frames. It could also be interesting to study metric neighbourhood frames.
The neighbourhood frames of modal logic are coalgebras for the functor [HK04,Lem.3.4]. Here, . On functions, we have
There are three well-known ways of extending powerset to orders. In domain theory, they are known as the upper, lower and convex powerdomain, and also known under the names of Hoare, Smyth and Plotkin, respectively. They correspond to the downset functor , the upset functor and the convex powerset functor . The first two arise from ordering powerset by inclusion and reverse inclusion. The third arises as the posetification of the powerset.
Similarly, there are three ways to extend the monotone neighbourhood functor to posets.
Recall that on objects and . As a functor (and as a monad)
and
On discrete , we have , so both are legitimate order generalisations of the functor .
Finally, there is also the posetification .
We derive the notions of cospan (bi)simulation of the functors and and .
Proposition: is a morphism of -coalgebras iff
is a morphism of -coalgebras iff
is a morphism of -coalgebras if
Morphisms of and -coalgebras coincide on discrete coalgebras. Here is an attempt at a visual summary:
In sets every function is a relation and every coalgebra morphism a bisimulation. In ordered sets every function gives rise to two relation and with
We have shown in Cospan Bisimulations 2 that these relations are cospan (bi)simulations if is a coalgebra morphism. This example suggests that more is true.
Proposition: is a morphism of -coalgebras iff and are cospan-(bi)simulations.
Proof: We only need to instantiate the characterisation of -cospan-(bi)simulation from the section on Bisimulation for Ordered Coalgebras.
An analogous statement is true for -coalgebras (CHECK).
(WHERE DO WE SEE THE DIFFERENCE BETWEEN THE TYPES OF COALGEBRAS IN THE LOGICS?)
Def: The two-sorted modal logic for ordered neighbourhood frames has point-formulas and set-formulas given as
and axioms saying that preserves finite meets and preserves finite joins.
Remark: This logic can be derived from the semantics using the principles of functorial modal logic (FML). This construction then guarantees the following proposition.
Prop: Formulas are invariant under morphisms and behavioural equivalence. Moreover, the logic is sound and complete for ordered neighbourhood models.
Dahlqvist and Kurz: The Positivication of Coalgebraic Logics. CALCO 2017. (Section 3.3 and 3.4)
Hansen, Kupke: A Coalgebraic Perspective on Monotone Modal Logic. 2004.
M. Pauly. Bisimulation for general non-normal modal logic. Manuscript, 1999.