Expressive Predicate Liftings

(draft … references to be added … up … predicate liftings … monotone predicate liftings)

For every functor

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

$n$ runs over all positive integers and the product is taken over all finitary predicate liftings)

$$TX\to \prod 2^{({2^n}^X)}$$

which, for a choice of predicate lifting

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

$\varphi :X\to 2^n$, applies

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

to elements of

$TX$.

Proposition: The natural transformation is injective on all finite

$X\ne \mathrm{\varnothing }$. ^[1]

Proof: Let

$s\ne t\in TX$. We have to show that there are

$n$,

$\varphi$ and

$\mathrm{△}$ such that

$\mathrm{△}(T\varphi (s))\ne \mathrm{△}(T\varphi (t))$. We choose

$n$ and

$\varphi$ so that

$\varphi :X\to 2^n$ is injective. Since

$X\ne \mathrm{\varnothing }$ it follows that also

$T\varphi$ is injective, that is,

$T\varphi (s)\ne T\varphi (t)$. Finally, we choose some

$\mathrm{△}:T(2^n)\to 2$ that separates the two.

Remark: This proofs shows that any two distinct elements of

$TX$ are separated by some predicate

$X\to 2^n$ and predicate lifting

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

Remark: For finitary functors

$T$ we can drop the restriction to finite sets.

Corollary: For a finitary functor

$T:\mathsf{S}\mathsf{e}\mathsf{t}\to \mathsf{S}\mathsf{e}\mathsf{t}$ the logic of all predicate liftings is expressive in the sense that for any two non-bisimular points there is a distinguishing formula.

(I can add a proof sketch if that turns out to be of interest.)

References

The results of this section are due to

• Lutz Schroeder: Expressivity of coalgebraic modal logic. 2008.

An axiomatic approach generalising to other categories than Set was presented by

• Bartek Klin: link text

The results can also be extended to the poset-enriched situation

• Kapulkin, Kurz, Velebil: link text

where expressivity is the stronger property that the logic does not only detect bisimulation but also simulation.

---

1. One can eliminate this proviso

   $X\ne \mathrm{\varnothing }$ by restricting to standard functors. Every set functor has a canonical standard functor which, moreover, induces an equivalent category of coalgebras. ↩︎