Monotone Predicate Liftings

(draft)

In a previous note, we defined predicate liftings and showed that the unary predicate liftings of the powerset functor are isomorphic to the free Boolean algebra generated by $\Box$ and $\Diamond$.

Here, we first single out all of those 16 modal operators that are monotone.

Then we are going to test our insights by studying the predicate liftings of two posets functors, namely the upset functor $\mathcal U$ and the downset functor $\mathcal D$.

Set Functors¶

We have studied modal operators as predicate liftings

where $\mathcal P 2$ can be pictured as ^[1]

Which order on $\mathcal P2$ exhibits the monotone modal operators as exactly the monotone predicate liftings?

The answer is given by the so-called posetification ^[2]

of the functor $\mathcal P:\sf Set\to Set$.

Fact: $\overline{\mathcal P}$ is the convex powerset functor, that is, for two convex subsets $a,b\subseteq X$ we have

Exercise: Recall that $2=\{0<1\}$. The order on $\overline{\mathcal P}2$ is given by $\{0\}<\{0,1\}<\{1\}$:


It follows that there are $2\times 4$ monotone predicate liftings $\overline{\mathcal P}2\to 2$. The 4 upsets of the chain are

We can now list all monotone predicate liftings as follows.

Summary¶

We have seen that in the example of the powerset functor that the monotone modal operators correspond precisely to the monotone functions $\overline{\mathcal P}2\to 2$ where $\overline{\mathcal P}$ is the convex powerset functor.

More generally, for any set-functor $T$, the $n$-ary monotone modal operators (=predicate liftings) are in bijection to the monotone functions

where $\overline T$ is the posetification of $T$.

Poset Functors¶

The Upset Functor¶

Let $\mathcal U$ be the upset functor. Consider

$\mathcal U2$ is the poset (again $\overline{01}=\{0,1\}$, etc)

which allows us to identify monotone functions $\mathcal U2\longrightarrow 2$ with upsets:

The difference between upsets of $\overline{\mathcal P}2$ and upsets of $\mathcal U 2$ is that in the latter case the “observation”

is not an upset of $\mathcal U 2$.

The Downset Functor¶

Let $\mathcal D$ be the downset functor. Consider

$\mathcal D2$ is the poset

which allows us to identify monotone functions $\mathcal D2\longrightarrow 2$ with upsets:

The difference between upsets of $\overline{\mathcal P}2$ and upsets of $\mathcal D 2$ is that in the latter case

is not available since $\overline 1$ is not an element of $\mathcal D2$.

Breakdown of Duality¶

It is interesting to think about why the arguments for $\mathcal U2$ and $\mathcal D2$ are not entirely dual.

On the “object level” there is duality: Swapping 0 and 1 and turning the order around is an isomorphism.

This means that it must be the “meta level” which is breaking the duality.

Importantly, for both $\mathcal U$ and $\mathcal D$, the meaning of the predicate liftings depends on the existential quantifier implicit in taking the direct image of $\phi$. For example, the statement

is on the meta level and does not dualise. ^[3]

We summarise the situation with the following picture, depicting $\mathcal P2$, $\mathcal U2$, $\mathcal D2$ and the subsets that correspond to $\Box$ and $\Diamond$:

Distribution Functor¶

Proposition: The posetification of the distribution functor is given by $p\sqsubseteq q$ if $p[S]\le q[S]$ for all upsets $S$.

This order on distributions goes back to (Jones and Plotkin, 1989) for so-called IPOs and was extended to all posets in Worrell 2000. The observation that it is the posetification will appear in (Kurz and Motamed, 2022).

References¶

The definition of the posetification (extension from $\sf Set$ to $\sf Pos$) of an arbitrary set-functor as well as the result on monotone predicate liftings is in

• Balan, Kurz, Velebil: Positive Fragments of Coalgebraic Logics. 2015.

Theorem 7.1 contains the result that the predicate liftings of the posetification of $T$ are the monotone predicate liftings of $T$.

Moreover, one can reconstruct the poset $(X,R)$ as a certain order-enriched colimit of the diagram $p_1,p_2:R\to X$. Then the posetification $\overline TX$ is defined as the said colimit of $Tp_1,Tp_2:TR\to TX$.

The posetification enjoys the universal property of an order-enriched left Kan extension.