What is predicate lifting?

Question

I have tried and tried again to understand coalgebraic logic (generalization of modal logics) but I can not understand the notions "predicate lifting" and "relation lifting". Are there explanations and illustrations for those notions, is this notion used outside coalgebraic logics community?

Chapter 6 of http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf is about predicate lifting, but the notion seems to be so remote from everything that I know. Can someone, please, reformulate this notion in more understandable terms?

Answer 1

Before going fully general with fibrations, one can understand predicate liftings entirely in sets. I'm writing $2^X$ for the set of predicates on $X$, that is, characteristic functions $X\to 2$ assigning every element of $X$ to its truth-value (i.e. whether the predicate holds or not).

In this sense, a predicate lifting for a functor $F: \mathsf{Set}\to\mathsf{Set}$ is a natural transformation $\lambda_X: 2^X \to 2^{FX}$, that "lifts" predicates from the set-level ($2^X$) to a predicate on functor elements ($2^{FX}$). If you have a predicate $P\in 2^X$, then $\lambda_X(P)$ is a predicate on $FX$. In coalgebraic modal logics, the predicate liftings provide the semantics to modal operators. For example, the modal formula $\Diamond\phi$ means that there is some successor (or "next world") satisfying $\phi$. If $P$ captures the semantics of $\phi$, then a predicate lifting $\lambda$ for $\Diamond$ would send $P$ to $\lambda_X(P)\in 2^{FX}$ and $\lambda_X(P)$ intuitively has those successor structures $s\in FX$ in which at least one successor satisfies $P$ (i.e. $\phi$).

If $\mathcal{P}$ denotes the (covariant) power set functor, then you can implement the predicate lifting for $\Diamond$ as $$ \lambda_X(P) = \{ s \in \mathcal{P}X : \exists x\in s\colon x\in P\} $$ Different modal operators have different semantics of course, and for $\Box\phi$ (all successor worlds satisfy $\phi$) one would define a predicate lifting as follows: $$ \lambda_X'(P) = \{ s\in \mathcal{P}X : \forall x\in s\colon x\in P\} $$ Instead of $\mathcal{P}$ you can put in other functors $F$ of course (with adjusted definitions of $\lambda_X$ and $\lambda_X'$).

Such a predicate lifting $\lambda_X$ 'lifts' the functor $F: \mathsf{Set}\to \mathsf{Set}$ to a functor $\bar F: \mathsf{Pred}\to \mathsf{Pred}$ on the category of predicates, which is a fibration over $\mathsf{Set}$. In the text you linked it seems that another generalization is done: $2^{(-)} = hom(-,2)$ gives rise to a fibration, and so you can generalize the truth values $2$ or even the base category.

Answer 2

I understand the constructions involved in this sort of thing best by way of induction rather than coinduction; the differences aren't huge, but examples of induction come to mind more easily. Perhaps the easiest way to see what predicate lifting is doing there is to look at the usual induction over the natural numbers.

So let's say we have a fibration $p:\mathcal{E}\to\mathcal{B}$, which has finite products, coproducts, and a natural numbers object $N$ in $\mathcal B$; fibred finite products and coproducts; and adjunctions $p\dashv \top_{(-)}\dashv C$. I'll also assume that it's a preorder fibration for simplicity, though it need not be. Say we have some predicate $P$ over $N$, and we want to know that $P$ holds of all $n\in N$; that is, our goal is to show that $\top_N\leqslant P$, where $\top_N$ is the uniformly true predicate on $N$.

To make use of induction we need to show that $\top_1\leqslant P(0)$ and that $P(-)\leqslant P(s(-))$, where $0,s$ are the zero and successor of $\mathcal B$'s NNO. Notice that, fibrationally speaking, this is the same as an arrow $\top_1\to P$ in the total category that sits over $0:1\to N$, and an arrow $P\to P$ that sits over $s:N\to N$. So in some sense, it looks a lot like the induction hypotheses also have their own algebraic form, following the form of the algebra in the base category. And this turns out to be just what's happening.

Really, what Jacobs calls "predicate lifting" is lifting a functor on the base category to the total category of predicates; under the above assumptions, the inductive hypotheses for induction can be packaged as an algebra for an endofuctor $\hat{(-)}:\mathcal{E}\to\mathcal{E}$. In this particular instance, the new predicate produced by the lifted functor has the following behavior: $\hat P(*)$ is true, while $\hat P(n)\Leftrightarrow P(n)$. Its not hard to see that the induction hypothesis is true exactly when $\hat P(-) \leqslant P([0,s](-))$ (i.e. when there's an arrow $\hat P\to P$ over $[0,s]$).

The validity of induction in a fibration with the properties described above comes from there being an initial algebra for $\hat{(-)}$ lying over $[0,s]:1+N\to N$. In particular, there will be a functor $G:\mathbf{Alg}(1+-)\to\mathbf{Alg}(F)$, and this functor will have a right adjoint. (And between Jacobs' full result, and those of Neil Ghani, we can generalize this well beyond the case of induction on $N$.)

So "all" that's going on with predicate lifting is that it's a nice way to explain, by way of various adjunctions, why the (co)algebra structure in the base category has anything to do with the structure of the predicates.

Hopefully this sheds some small amount of light on the idea. Let me know if there's any way I can clarify things.