# Monotone Predicate Liftings

(draft ...[up](https://hackmd.io/@alexhkurz/ryrkkYZZc) ... [predicate liftings](https://hackmd.io/@alexhkurz/SJcARPMVO) ... [expressive predicate liftings](https://hackmd.io/@alexhkurz/rkPk_3sNd))

In a previous note, we defined [predicate liftings](https://hackmd.io/@alexhkurz/SJcARPMVO) 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
$$\mathcal P 2\to 2$$

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


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 [^posetification]
$$\overline{\mathcal P}:\sf Pos\to Pos$$

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
\begin{align}
a\le b\ \quad \textrm{ iff } \quad & \forall x\in a\,.\,\exists y\in b. x\le y \quad \textrm{ and }\\
&\forall y\in b\,.\,\exists x\in a. x\le y\\
\end{align}

**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
$$ \{\overline 0,\overline{01},\overline 1\}, \{\overline{01},\overline 1\}, \{\overline 1\}, \{\}$$

We can now list all monotone predicate liftings as follows.

|subset of $\mathcal P2$| Boolean combination of generators | modal formula
|:---:|:---:|:---:|
|$\{\}$| $\bot$ | $\bot$ |
|$\{\overline 1\}$| $\sf \neg o\wedge i$ | $\Box\phi\wedge\Diamond\phi$ |
|$\{\overline{01},\overline 1\}$| $\sf i$ | $\Diamond\phi$ |
|$\{\overline 0,\overline{01},\overline 1\}$| $\sf o\vee i$ | $\Diamond\top$ |
|$\{\varnothing\}$| $\sf \neg o\wedge\neg i$ | $\Box\bot$ |
|$\{\varnothing,\overline 1\}$| $\sf \neg o$ | $\Box\phi$ |
|$\{\varnothing,\overline{01},\overline 1\}$| $\sf \neg o\vee i$ | $\Box\phi\vee\Diamond\phi$ |
|$\{\varnothing,\overline 0,\overline{01},\overline 1\}$| $\top$ | $\top$ |

## 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
$$\overline T(2^n)\to 2$$

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

## Poset Functors

### The Upset Functor

Let $\mathcal U$ be the upset functor. Consider
$$\mathcal UX\stackrel{\mathcal U\phi}\longrightarrow\mathcal U2\longrightarrow 2$$

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

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

|upset of $\mathcal U2$| modal formula
|:---:|:---:|
|$\{\overline{01},\overline 1,\varnothing\}$| $\top$ |
|$\{\overline 1,\varnothing\}$| $\Box\phi$ |
|$\{\varnothing\}$|$\Box\bot$ |
|$\{\}$| $\bot$ |

The difference between upsets of $\overline{\mathcal P}2$ and upsets of $\mathcal U 2$ is that in the latter case the "observation"
$$\{\overline{01},\overline{1}\}=\sf (o\wedge i)\vee (\neg o\wedge i) = i \quad \textrm{ which corresponds to } \quad \Diamond\phi$$

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

### The Downset Functor

Let $\mathcal D$ be the downset functor. Consider
$$\mathcal DX\stackrel{\mathcal D\phi}\longrightarrow\mathcal D2\longrightarrow 2$$

$\mathcal D2$ is the poset
$$\varnothing<\overline{0}<\overline{01}$$

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

|upset of $\mathcal D2$| modal formula
|:---:|:---:|
|$\{\varnothing,\overline 0,\overline{01}\}$| $\top$ |
|$\{\overline 0,\overline{01}\}$| $\Diamond\top$ |
|$\{\overline{01}\}$| $\Diamond\phi$ |
|$\{\}$| $\bot$ |

The difference between upsets of $\overline{\mathcal P}2$ and upsets of $\mathcal D 2$ is that in the latter case
$$\{\varnothing,\overline{1}\}=\sf (\neg o\wedge \neg i)\vee (\neg o\wedge i) = \neg o \quad \textrm{ which corresponds to } \quad \Box\phi$$

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
$$\phi[S]=\overline 1
\quad
\textrm{ only if }
\quad
\phi[S]\subseteq \overline{01}$$

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

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](https://lmcs.episciences.org/1594). 2015.

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

[^predlift]: Recall that for a predicate lifting $\triangle$ and a formula $\varphi:X\to 2$, the meaning of $\triangle\phi$ is given by how the composition $\mathcal PX\stackrel{\mathcal P\phi}\longrightarrow{\mathcal P2}\stackrel \triangle\longrightarrow 2$ acts on a subset 'of successors' $S\in\mathcal PX$.

[^posetification]: The posetification of a functor $T$ is defined as follows. Any poset $(X,R)$ can be represented by its "graph"
$$p_1,p_2:R\to X$$

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.

[^doesnot]: "$\phi[S]=\overline 1$ only if $\phi[S]\subseteq \overline{01}$" is needed to establish that $\{\overline{01}\}\subseteq\mathcal D2$ corresponds to $\Diamond\phi$.