Monotone Predicate Liftings

(draft …up … predicate liftings … expressive predicate liftings)

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

$◻$ and

$◊$.

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 ^[1]

Which order on

$\mathcal{P}2$ exhibits the monotone modal operators as exactly the monotone predicate liftings?

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

$$\bar{\mathcal{P}}:\mathsf{P}\mathsf{o}\mathsf{s}\to \mathsf{P}\mathsf{o}\mathsf{s}$$

of the functor

$\mathcal{P}:\mathsf{S}\mathsf{e}\mathsf{t}\to \mathsf{S}\mathsf{e}\mathsf{t}$.

Fact:

$\bar{\mathcal{P}}$ is the convex powerset functor, that is, for two convex subsets

$a,b\subseteq X$ we have

$$\begin{array}{rl}a\le b\text{ iff }& \mathrm{\forall }x\in a.\mathrm{\exists }y\in b.x\le y\text{ and }\\ & \mathrm{\forall }y\in b.\mathrm{\exists }x\in a.x\le y\end{array}$$

Exercise: Recall that

$2=\{0<1\}$. The order on

$\bar{\mathcal{P}}2$ is given by

$\{0\}<\{0,1\}<\{1\}$:

It follows that there are

$2\times 4$ monotone predicate liftings

$\bar{\mathcal{P}}2\to 2$. The 4 upsets of the chain are

$$\{\bar{0},\overline{01},\bar{1}\},\{\overline{01},\bar{1}\},\{\bar{1}\},\{\}$$

We can now list all monotone predicate liftings as follows.

subset of $\mathcal{P}2$	Boolean combination of generators	modal formula
$\{\}$	$\mathrm{\perp }$	$\mathrm{\perp }$
$\{\bar{1}\}$	$\mathrm{\neg }\mathsf{o}\wedge \mathsf{i}$	$◻\varphi \wedge ◊\varphi$
$\{\overline{01},\bar{1}\}$	$\mathsf{i}$	$◊\varphi$
$\{\bar{0},\overline{01},\bar{1}\}$	$\mathsf{o}\vee \mathsf{i}$	$◊\mathrm{\top }$
$\{\varnothing \}$	$\mathrm{\neg }\mathsf{o}\wedge \mathrm{\neg }\mathsf{i}$	$◻\mathrm{\perp }$
$\{\varnothing ,\bar{1}\}$	$\mathrm{\neg }\mathsf{o}$	$◻\varphi$
$\{\varnothing ,\overline{01},\bar{1}\}$	$\mathrm{\neg }\mathsf{o}\vee \mathsf{i}$	$◻\varphi \vee ◊\varphi$
$\{\varnothing ,\bar{0},\overline{01},\bar{1}\}$	$\mathrm{\top }$	$\mathrm{\top }$

Summary

We have seen that in the example of the powerset functor that the monotone modal operators correspond precisely to the monotone functions

$\bar{\mathcal{P}}2\to 2$ where

$\bar{\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

$$\bar{T}(2^n)\to 2$$

where

$\bar{T}$ is the posetification of

$T$.

Poset Functors

The Upset Functor

Let

$\mathcal{U}$ be the upset functor. Consider

$$\mathcal{U}X\stackrel{\mathcal{U}\varphi }{⟶}\mathcal{U}2⟶2$$

$\mathcal{U}2$ is the poset (again

$\overline{01}=\{0,1\}$, etc)

$$\overline{01}<\bar{1}<\varnothing$$

which allows us to identify monotone functions

$\mathcal{U}2⟶2$ with upsets:

upset of $\mathcal{U}2$	modal formula
$\{\overline{01},\bar{1},\varnothing \}$	$\mathrm{\top }$
$\{\bar{1},\varnothing \}$	$◻\varphi$
$\{\varnothing \}$	$◻\mathrm{\perp }$
$\{\}$	$\mathrm{\perp }$

The difference between upsets of

$\bar{\mathcal{P}}2$ and upsets of

$\mathcal{U}2$ is that in the latter case the "observation"

$$\{\overline{01},\bar{1}\}=\mathsf{(}\mathsf{o}\wedge \mathsf{i}\mathsf{)}\vee \mathsf{(}\mathrm{\neg }\mathsf{o}\wedge \mathsf{i}\mathsf{)}\mathsf{=}\mathsf{i}\text{ which corresponds to }◊\varphi$$

is not an upset of

$\mathcal{U}2$.

The Downset Functor

Let

$\mathcal{D}$ be the downset functor. Consider

$$\mathcal{D}X\stackrel{\mathcal{D}\varphi }{⟶}\mathcal{D}2⟶2$$

$\mathcal{D}2$ is the poset

$$\varnothing <\bar{0}<\overline{01}$$

which allows us to identify monotone functions

$\mathcal{D}2⟶2$ with upsets:

upset of $\mathcal{D}2$	modal formula
$\{\varnothing ,\bar{0},\overline{01}\}$	$\mathrm{\top }$
$\{\bar{0},\overline{01}\}$	$◊\mathrm{\top }$
$\{\overline{01}\}$	$◊\varphi$
$\{\}$	$\mathrm{\perp }$

The difference between upsets of

$\bar{\mathcal{P}}2$ and upsets of

$\mathcal{D}2$ is that in the latter case

$$\{\varnothing ,\bar{1}\}=\mathsf{(}\mathrm{\neg }\mathsf{o}\wedge \mathrm{\neg }\mathsf{i}\mathsf{)}\vee \mathsf{(}\mathrm{\neg }\mathsf{o}\wedge \mathsf{i}\mathsf{)}\mathsf{=}\mathrm{\neg }\mathsf{o}\text{ which corresponds to }◻\varphi$$

is not available since

$\bar{1}$ is not an element of

$\mathcal{D}2$.

Breakdown of Duality

It is interesting to think about why the arguments for

$\mathcal{U}2$ and

$\mathcal{D}2$ 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

$\varphi$. For example, the statement

$$\varphi [S]=\bar{1}\text{ only if }\varphi [S]\subseteq \overline{01}$$

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

We summarise the situation with the following picture, depicting

$\mathcal{P}2$,

$\mathcal{U}2$,

$\mathcal{D}2$ and the subsets that correspond to

$◻$ and

$◊$:

Distribution Functor

Proposition: The posetification of the distribution functor is given by

$p⊑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

$\mathsf{S}\mathsf{e}\mathsf{t}$ to

$\mathsf{P}\mathsf{o}\mathsf{s}$) 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$.

---

1. Recall that for a predicate lifting

   $\mathrm{△}$ and a formula
   $\phi :X\to 2$, the meaning of
   $\mathrm{△}\varphi$ is given by how the composition
   $\mathcal{P}X\stackrel{\mathcal{P}\varphi }{⟶}\mathcal{P}2\stackrel{\mathrm{△}}{⟶}2$ acts on a subset 'of successors'
   $S\in \mathcal{P}X$. ↩︎

2. 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
   $\bar{T}X$ is defined as the said colimit of
   $T{p}_1,T{p}_2:TR\to TX$.

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

3. "

   $\varphi [S]=\bar{1}$ only if
   $\varphi [S]\subseteq \overline{01}$" is needed to establish that
   $\{\overline{01}\}\subseteq \mathcal{D}2$ corresponds to
   $◊\varphi$. ↩︎