$$

Coalgebraic Logic: Predicate Liftings

(draft … up … next monotone predicate liftings and expressive predicate liftings)

Definition

A

$n$-ary predicate lifting for a functor

$T:\mathsf{S}\mathsf{e}\mathsf{t}\to \mathsf{S}\mathsf{e}\mathsf{t}$ is a natural transformation

$${2^n}^X\to 2^{TX}$$

It follows from the Yoneda lemma that such natural transformations are in bijection with functions

$$T(2^n)\to 2.$$

In one direction, we apply

${2^n}^X\to 2^{TX}$ to the idenity on

$X=2^n$ to obtain

$T(2^n)\to 2$.

In the other direction, each

$T(2^n)\to 2$ induces a modal operator as follows.

Given a predicate lifting

$\mathrm{△}:T(2^n)\to 2$ and a collection

$\varphi :X\to 2^n$ of

$n$ predicates

${\varphi }_i:X\to 2$, we obtain

$TX\to 2$ defined as

$$TX\stackrel{T\varphi }{⟶}T(2^n)\stackrel{\mathrm{△}}{⟶}2$$

Precomposing with a coalgebra

$X\to TX$ the semantics of a modal formula

$$\mathrm{△}\varphi$$

is then given by

$$X⟶TX\stackrel{T\varphi }{⟶}T(2^n)\stackrel{\mathrm{△}}{⟶}2.$$

A good way to understand what is going on here is to explicitely calculate all unary predicate liftings of the powerset functor.

But before doing this let us clarify terminology.

First, to simplify notation, we will only consider unary predicate liftings in the following.

Terminology: We tend to say predicate lifting for the function

$$\mathrm{△}:T2\to 2$$

and modal operator (or sometimes predicate transformer) for the function that maps a predicate

$\varphi$ to the predicate

$$\mathrm{△}\varphi :X\to TX\stackrel{T\varphi }{⟶}T2\stackrel{\mathrm{△}}{⟶}2.$$

Question: Would it be better to reverse the terminology? Or perhaps as follows:

• predicate lifting
  $2^X\to 2^{TX}$
• predicate transformer
  $2^X\to 2^{TX}\to 2^X$
• modal operator:
  $T2\to 2$

Anyway: Since there is a bijection between predicate liftings and modal operators, we may blur the distinction on occasion.

Example: Powerset

Let

$T=\mathcal{P}$ be the powerset functor.

We see right away that there are 16 modal operators

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

because that is the cardinality of the set of functions of type

$\mathcal{P}2\to 2$.

We are interested in explicitely describing all modal operators

$\mathrm{△}:\mathcal{P}2\to 2$ taking predicates

$\varphi :X\to 2$ to

$$\mathcal{P}X\stackrel{\mathcal{P}\varphi }{⟶}\mathcal{P}2\stackrel{\mathrm{△}}{⟶}2$$

We need to know that

$\mathcal{P}\varphi$ takes direct image. This tells us how to interpret the 4 possible results of applying

$\mathcal{P}\varphi$ to a set

$S$ of successors. Writing

$2=\{0,1\}$, if

$(\mathcal{P}\varphi )S$ is ^[1]

• $\{0,1\}$ then some successors are outside of
  $\varphi$ and some are inside of
  $\varphi$.
• $\{0\}$ then all and some successors are out.
• $\{1\}$ then all and some successors are in.
• $\{\}$ then there are no successors.

For the purpose of further calculations I propose the following abbreviations:

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

for the elements of

$\mathcal{P}2$.

Exercise: (Assumes familiarity with the classical definition of the modal operators

$◻$ and

$◊$). Show that

$\varnothing ,\bar{1}\mapsto 1$ defines

$◻$ and that

$\bar{1},\overline{01}\mapsto 1$ defines

$◊$. ^[2]

Answer. ^[3]

Observation: The modal operator

$◻:\mathcal{P}2\to 2$ coincides with

$\bigwedge :\mathcal{P}2\to 2$ and the modal operator

$◊:\mathcal{P}2\to 2$ coincides with

$\bigvee :\mathcal{P}2\to 2$.

Modal logic is expressive up to bisimilarity and this means here that all predicate liftings

$\mathcal{P}2\to 2$ (and also all

$\mathcal{P}{2}^n\to 2$) are generated by those for

$◻$ and

$◊$. Let us try to support this with some examples:

Exercise: Using

$◻,◊$ as well as propositional connectives, express the predicate liftings

${\mathrm{△}}_{\sigma }$ defined by

$\sigma \mapsto 1$ where

$\sigma$ ranges over

$\{\varnothing ,\bar{0},\overline{01},\bar{1}\}$. Also verify that

$◊=\mathrm{\neg }◻\mathrm{\neg }$ holds for the corresponding predicate liftings.

Our next concern is to better understand the lattice (Boolean algebra) of all unary modal operators of the powerset functor

$\mathcal{P}$.

We already noted that there are 16 unary modal operators

$P2\to 2$ and we exhibited some salient examples.

From general facts about Boolean algebras we can deduce the following. The Boolean algebra of modal operators

$P2\to 2$ is isomorphic to the free Boolean algebra on two generators, which I call

$\mathsf{o}$ and

$\mathsf{i}$. ^[4] These generators combine to the atoms of the Boolean algebra as

$$\mathsf{o}\wedge \mathsf{i}\mathsf{,}\mathsf{o}\wedge \mathrm{\neg }\mathsf{i}\mathsf{,}\mathrm{\neg }\mathsf{o}\wedge \mathsf{i}\mathsf{,}\mathrm{\neg }\mathsf{o}\wedge \mathrm{\neg }\mathsf{i}\mathsf{.}$$

Every element of the Boolean algebra of modal operators is a join of these atoms.

Exercise: Define an isomorphism between predicate liftings

$\mathcal{P}2\to 2$ and the free Boolean algebra generated by

$\{\mathsf{o}\mathsf{,}\mathsf{i}\}$ which maps

$◻$ to

$\mathrm{\neg }\mathsf{o}$ and

$◊$ to

$\mathsf{i}$.

Answer. ^[5]

Remark: The isomorphism in the previous exercise has been chosen in such a way that the generator

$\mathsf{o}$ is interpreted as "some successors are outside of

$\varphi$" and

$\mathsf{i}$ as "some successors are inside".

1. This choice of interpretation is suggested by how the functor
   $\mathcal{P}$ acts on
   $\varphi$ (as direct image). In particular,
   $\mathsf{o}$ symbolizes the observation that the direct image under
   $\varphi$ of the set of successors contains
   $0$ and
   $\mathsf{i}$ that the direct image contains
   $1$.
2. From the point of view of Boolean generators there is no reason to prefer
   $\mathrm{\neg }\mathsf{o}$ over
   $\mathsf{o}$. But from a logician's point of view
   $\mathrm{\neg }\mathsf{o}$, which is
   $◻$, has the advantage of being a monotone operator. We will study this in more detail in the follow-up note on monotone predicate liftings.

Remark: Items 1. and 2. could be the starting point for a rational reconstruction of why classical modal logic is usually presented in terms of

$◻$ and

$◊$. One would begin with the question of a logic that is invariant under bisimilarity, answer that such a logic is given by the logic of all predicate liftings and then proceed to the insight that

$◻$ and

$◊$ generate all predicate liftings in a canonical way.

Summary: We introduced some notation for the set

$\mathcal{P}2$

and then represented the unary modal operators as subsets of

$\mathcal{P}2$. For example,

• $◻=\{\varnothing ,\bar{1}\}=\mathrm{\neg }\mathsf{o}$ ("nothing out")
• $◊=\{\bar{1},\overline{01}\}=\mathsf{i}$ ("at least one in")

As a corollary we identified

$◻$ and

$◊$ as the generators of the free Boolean algebra of all unary predicate liftings.

Puzzle: If we equip

$\mathcal{P}2$ with the inclusion order, then

$◻$ is not a monotone function

$\mathcal{P}2\to 2$ (when

$2$ is ordered as

$0<1$). On the other hand, we do know that

$◻$ is a monotone modal operator in the sense that ^[6]

$$\frac{\varphi \to \psi }{◻\varphi \to ◻\psi }$$

This puzzle will be resolved in a follow-up note on monotone predicate liftings.

Example: Probability Distributions

Let

$\mathcal{D}$ be the functor that maps a set

$X$ to the set

$\mathcal{D}X$ of finitely supported probability distributions.

The unary modalities are given by sets of distributions on 2

$$\mathcal{D}2\to 2.$$

A modal operators

$\mathrm{△}:\mathcal{D}2\to 2$ takes a predicate

$\varphi :X\to 2$ to

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

The atoms of the Boolean algebra are the sets

$\{b_r\}$ where

$b_r(1)=r$. If

$\mathrm{△}$ is

$\{b_r\}$, then

$$p\in [[\mathrm{△}\varphi ]]\iff Pr(x\in \varphi )=r$$

---

1. This reminds me of the square of opposition in Aristotelian logic.

   $\{1\}$ corresponds to
   $\varphi$ "belongs to all successors",
   $\{0\}$ to
   $\varphi$ "belongs to no successors",
   $\mathrm{\top }$ to "belongs to some but not all". As far as I understand (not my area of expertise) Aristotle's logic does not admit
   $\varnothing$. ↩︎

2. Here and in the following all elements not explicitly mentioned are sent to

   $0$. For example, writing
   $\varnothing ,\bar{1}\mapsto 1$ implies
   $\bar{0},\overline{01}\mapsto 0$. ↩︎

3. For example, in the case of

   $◻$, one has to verify that with
   $\mathrm{△}$ defined as
   $\varnothing ,\bar{1}\mapsto 1$ the function
   $\mathcal{P}X\stackrel{\mathcal{P}\varphi }{⟶}\mathcal{P}2\stackrel{\mathrm{△}}{⟶}2$ maps
   $S\subseteq X$ to
   $1$ iff
   $S\subseteq \varphi$. ↩︎

4. Intuitively,

   $\mathsf{o}$ means "some successor outside of
   $\varphi$" and
   $\mathsf{i}$ means "some successor inside
   $\varphi$". It is a lucky coincidence that the symbol
   $\mathsf{o}$ reminds us of both out and
   $0$ and
   $\mathsf{i}$ of both in and
   $1$. ↩︎

5. Recall that

   $\varnothing$ means "no successor",
   $\bar{0}$ means "some and all successor outside of
   $\varphi$",
   $\bar{1}$ means "some and all successors in
   $\varphi$" and
   $\overline{01}$ means "some out and some in".
   Accordingly, we map the elements
   $\varnothing ,\bar{0},\overline{01},\bar{1}\in \mathcal{P}2$ to conjunctions of generators as follows.
   $\varnothing \mapsto \mathrm{\neg }\mathsf{o}\wedge \mathrm{\neg }\mathsf{i}$,
   $\bar{0}\mapsto \mathsf{o}\wedge \mathrm{\neg }\mathsf{i}$,
   $\overline{01}\mapsto \mathsf{o}\wedge \mathsf{i}$,
   $\bar{1}\mapsto \mathrm{\neg }\mathsf{o}\wedge \mathsf{i}$. ↩︎

6. It also makes sense to replace

   $\to$ by
   $\le$ if we think of predicates as propositional functions to
   $2=\{0<1\}$. ↩︎