Predicate Liftings - Coalgebraic Logic

(draft)

Definition¶

A $n$ -ary predicate lifting for a functor $T:\sf Set\to Set$ is a natural transformation

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

(1)

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

T(2^n)\to 2.

(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 $\triangle: T(2^n)\to 2$ and a collection $\phi:X\to 2^n$ of $n$ predicates $\phi_i:X\to 2$ , we obtain $TX\to 2$ defined as

TX\stackrel {T\phi}\longrightarrow T(2^n)\stackrel\triangle\longrightarrow 2

(3)

Precomposing with a coalgebra $X\to TX$ the semantics of a modal formula

\triangle \phi

(4)

is then given by

X\longrightarrow TX\stackrel {T\phi}\longrightarrow T(2^n)\stackrel\triangle\longrightarrow 2.

(5)

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

\triangle: T2\to 2

(6)

and modal operator (or sometimes predicate transformer) for the function that maps a predicate $\phi$ to the predicate

\triangle\phi: X\to TX \stackrel {T\phi}\longrightarrow T2\stackrel\triangle\longrightarrow 2.

(7)

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 P2\to 2

(8)

because that is the cardinality of the set of functions of type $\mathcal P2\to 2$ .

We are interested in explicitely describing all modal operators $\triangle:\mathcal P2\to 2$ taking predicates $\phi:X\to 2$ to

\mathcal PX\stackrel {\mathcal P\phi}\longrightarrow \mathcal P2\stackrel\triangle\longrightarrow 2

(9)

We need to know that $\mathcal P\phi$ takes direct image. This tells us how to interpret the 4 possible results of applying $\mathcal P \phi$ to a set $S$ of successors. Writing $2=\{0,1\}$ , if $(\mathcal P\phi)S$ is ^[1]

$\{0,1\}$ then some successors are outside of $\phi$ and some are inside of $\phi$ .
$\{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=\{\} \quad\quad \overline 0=\{0\} \quad\quad \overline{01}=\{0,1\} \quad\quad \overline 1=\{1\}

(10)

for the elements of $\mathcal P2$ .

Exercise: (Assumes familiarity with the classical definition of the modal operators $\Box$ and $\Diamond$ ). Show that $\varnothing,\overline 1\mapsto 1$ defines $\Box$ and that $\overline 1,\overline{01}\mapsto 1$ defines $\Diamond$ . ^[2]

Answer. ^[3]

Observation: The modal operator $\Box:\mathcal P2\to 2$ coincides with $\bigwedge: \mathcal P2\to 2$ and the modal operator $\Diamond:\mathcal P2\to 2$ coincides with $\bigvee: \mathcal P2\to 2$ .

Modal logic is expressive up to bisimilarity and this means here that all predicate liftings $\mathcal P2\to 2$ (and also all $\mathcal P2^n\to 2$ ) are generated by those for $\Box$ and $\Diamond$ . Let us try to support this with some examples:

Exercise: Using $\Box,\Diamond$ as well as propositional connectives, express the predicate liftings $\triangle_\sigma$ defined by $\sigma\mapsto 1$ where $\sigma$ ranges over $\{\varnothing,\overline 0, \overline{01},\overline 1\}$ . Also verify that $\Diamond=\neg\Box\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 $\sf o$ and $\sf i$ . ^[4] These generators combine to the atoms of the Boolean algebra as

\sf o\wedge i, o\wedge\neg i, \neg o\wedge i, \neg o\wedge\neg i.

(11)

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

Exercise: Define an isomorphism between predicate liftings $\mathcal P2\to 2$ and the free Boolean algebra generated by $\{\sf o,i\}$ which maps $\Box$ to $\neg\sf o$ and $\Diamond$ to $\sf i$ .

Answer. ^[5]

Remark: The isomorphism in the previous exercise has been chosen in such a way that the generator $\sf o$ is interpreted as “some successors are outside of $\phi$ ” and $\sf i$ as “some successors are inside”.

This choice of interpretation is suggested by how the functor $\mathcal P$ acts on $\phi$ (as direct image). In particular, $\sf o$ symbolizes the observation that the direct image under $\phi$ of the set of successors contains 0 and $\sf i$ that the direct image contains 1.
From the point of view of Boolean generators there is no reason to prefer $\sf \neg o$ over $\sf o$ . But from a logician’s point of view $\sf \neg o$ , which is $\Box$ , 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 $\Box$ and $\Diamond$ . 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 $\Box$ and $\Diamond$ generate all predicate liftings in a canonical way.

Summary: We introduced some notation for the set $\mathcal P2$

and then represented the unary modal operators as subsets of $\mathcal P2$ . For example,

$\Box=\{\varnothing,\overline 1\} = \neg \sf o$ (“nothing out”)
$\Diamond = \{\overline 1,\overline{01}\} = \sf i$ (“at least one in”)

As a corollary we identified $\Box$ and $\Diamond$ as the generators of the free Boolean algebra of all unary predicate liftings.

Puzzle: If we equip $\mathcal P2$ with the inclusion order, then $\Box$ is not a monotone function $\mathcal P2 \to 2$ (when 2 is ordered as $0<1$ ). On the other hand, we do know that $\Box$ is a monotone modal operator in the sense that ^[6]

\frac{\phi\to\psi}{\Box\phi\to\Box\psi}

(12)

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 DX$ of finitely supported probability distributions.

The unary modalities are given by sets of distributions on 2

\mathcal D2\to 2.

(13)

A modal operators $\triangle:\mathcal D2\to 2$ takes a predicate $\phi:X\to 2$ to

\mathcal DX\stackrel {\mathcal D\phi}\longrightarrow \mathcal D2\stackrel\triangle\longrightarrow 2

(14)

The atoms of the Boolean algebra are the sets $\{b_r\}$ where $b_r(1)=r$ . If $\triangle$ is $\{b_r\}$ , then

p\in \sem{\triangle\phi}\ \Leftrightarrow \ Pr(x\in\phi) =r

(15)

Footnotes¶

This reminds me of the square of opposition in Aristotelian logic. $\{1\}$ corresponds to $\phi$ “belongs to all successors”, $\{0\}$ to $\phi$ “belongs to no successors”, $\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$ .
↩
Here and in the following all elements not explicitly mentioned are sent to 0. For example, writing $\varnothing,\overline 1\mapsto 1$ implies $\overline 0,\overline{01}\mapsto 0$ .
↩
For example, in the case of $\Box$ , one has to verify that with $\triangle$ defined as $\varnothing,\overline 1\mapsto 1$ the function $\mathcal PX\stackrel {\mathcal P\phi}\longrightarrow \mathcal P2\stackrel\triangle\longrightarrow 2$ maps $S\subseteq X$ to 1 iff $S\subseteq\phi$ .
↩
Intuitively, $\sf o$ means “some successor outside of $\phi$ ” and $\sf i$ means “some successor inside $\phi$ ”. It is a lucky coincidence that the symbol $\sf o$ reminds us of both out and 0 and $\sf i$ of both in and 1.
↩
Recall that $\varnothing$ means “no successor”, $\overline 0$ means “some and all successor outside of $\phi$ ”, $\overline 1$ means “some and all successors in $\phi$ ” and $\overline{01}$ means “some out and some in”. Accordingly, we map the elements $\varnothing,\overline 0,\overline{01},\overline 1\in\mathcal P2$ to conjunctions of generators as follows. $\varnothing \mapsto \sf \neg o\wedge\neg i$ , $\overline 0\mapsto \sf o\wedge\neg i$ , $\overline{01}\mapsto \sf o\wedge i$ , $\overline 1\mapsto \sf\neg o\wedge i$ .
↩
It also makes sense to replace $\to$ by $\le$ if we think of predicates as propositional functions to $2=\{0<1\}$ .
↩