Introduction

We have seen in the chapter “Order Enriched Coalgebraic Logic” that much of coalgebraic logic generalizes from the sets and Boolean algebras to posets and distributive lattices.

The intention of this chapter is to generalize this from the two-element quantale to a general quantale. Much of this work in progress but the outlines of this general theory are emerging ...

A quantale $\Qu$ is a monoid in the category of complete join semilattices (suplattices). We write the order as $\sqsubseteq$, and the operations join and multiplication as $\bigsqcup$ and $\cdot$. The neutral elements are denoted by $\bot_\Qu,1_\Qu$, respectively, dropping the subscripts whenever convenient. Because a quantale is a complete lattice, we also have $\bigsqcap$ and because multiplication preserves joins in each argument we have residuals $\rhd$ and $\lhd$ defined by $a\cdot b \sqsubseteq c \ \Leftrightarrow\ a \sqsubseteq c\lhd b \ \Leftrightarrow \ b\sqsubseteq a\rhd c$

The Logic of Chosen Predicate Liftings¶

In this section, we list the ingredients needed to apply the framework of (functorial) coalgebraic logic to many-valued modal logics with truth-values in a quantale. The logic will be generated by a choice of propositional logic (via a suitable algebra) and a choice of predicate liftings (which will determine the meaning of the modal operators).

• $\Qu$, a quantale

• $\QuCat$, category of $\Qu$-enriched categories

• $T:\QuCat\to\QuCat$, a functor for coalgebras

• $\triangle:({\Qu^n})^X\to Q^{TX}$, $n$-ary predicate liftings

• $\mathcal A$, a category of algebras containing $\Qu$ such that there is

  • $F\dashv U:\mathcal A\to \Set$, so that $Fn$ is the free algebra on $n$-generators ^[1]

• $P:\QuCat\to\mathcal A$, a contravariant functor defined by $UPX=Q^X =\QuCat(X,\Qu)$

  • $n$-ary predicate liftings are of the form $U(PX)^n\to UPTX$.

• $L:\mathcal A\to \mathcal A$

  • $LA \stackrel {\text{def}} =\coprod_\triangle F(UA)^n$ aggregates the domains of all predicate liftings.^[2]

• $\delta:LP\to PT$ aggregates all predicate liftings into one natural transformation.

  • Each $n$-ary predicate lifting $({\Qu^n})^X\to Q^{TX}$ induces an $\mathcal A$-morphism $F(UPX)^n\to PTX$. ^[3]

  • All $F(UPX)^n\to PTX$ aggregate to $\delta:LP\to PT$. ^[4]

• $\widetilde P:\Coalg(T)\to\Alg(L)$, defined by $\widetilde P(X\to TX)=LPX\to PTX\to PX$

  • $\widetilde P(X\to TX)$ is called the “complex algebra” of $X\to TX$.

• The semantics of the logic wrt a coalgebra $X\to TX$ is given by the unique $\mathcal A$-morphism from the initial $L$-algebra to the complex algebra $\widetilde P(X\to TX)$.

Remark: In this minimal setting, the dualizing object $\Qu$ induces the functor $P:\QuCat\to\mathcal A$, but for now we do not insist on the existence of an adjoint to $P$.

A Principled Approach¶

In this section, we will study principled ways of defining the logic of all predicate liftings for any functor $T:\QuCat\to\QuCat$ for any quantale $\Qu$. Assumptions, if needed are imposed on the way.

... tbc ...