Boolean Logic for Set-Coalgebras

We build on concepts and examples explained previously, but try to keep this section self-contained from a technical point of view.

We specialise the setting from Coalgebraic Logic: Introduction as follows:

• a functor
  $T:Set\to Set$
• a functor
  $L:\mathsf{B}\mathsf{A}\to \mathsf{B}\mathsf{A}$
• $F⊣U:\mathsf{B}\mathsf{A}\to Set$
• $P:Set\to BA$ given by
  $PX=2^X$
• $S:BA\to Set$ given by
  $SA=BA(A,2)$
• ${\delta }_X:LPX\to PTX$

We have seen previously that modal logics for

$T$-coalgebras can be described by giving

$L$ and

$\delta$.

Conversely, every sifted colimit preserving functor on a variety has a presentation and hence gives rise to a modal logic. Before we see how this works let us state some results needed later.

Proposition: Let

$L$ be a sifted colimit preserving functor on

$\mathsf{B}\mathsf{A}$. There is a functor

$L^{\prime }$ that agrees with

$L$ on all non-trivial algebras and preserves filtered colimits. Moreover

$Alg(L)\cong Alg(L^{\prime })$.

Lemma: Let

$H$ be a functor on

$\mathsf{B}\mathsf{A}$ and

$L$ a sifted colimit preserving functor on

$\mathsf{B}\mathsf{A}$ and

$LFn=HFn$ for all finitely generated free Boolean algebras

$Fn$. Then

$LA=HA$ for all finite non-trivial algebras

$A$.

Proof: Every finite non-trivial Boolean algebra is a retract of a finitely generated free one.

The logic of

$L$

As promised, we are going to show that every sifted colimit preserving functor on a variety has a presentation and hence gives rise to a modal logic.

Every sifted colimit preserving functor

$L$ on a variety is a quotient

$$FGUA\stackrel{q_A}{⟶}LA$$

where

$GX=\coprod _{n\in \mathbb{N}}ULFn\times X^n$. Since

$F$ is a left adjoint, the morphism

$q_A$ is the adjoint transpose of a morphism

$$GUA⟶ULA$$

which determines (and is determinedy by) the following modal logic.

• The
  $n$-ary modal operators
  $\sigma$ are the elements of
  $ULFn$.
• $q_A$ maps
  $(\sigma ,v:n\to UA)$ to
  $L(v^{†})(\sigma )$ where
  $v^{†}$ is the adjoint transpose of
  $v$.
• The equations in
  $n$ variables are the kernel of
  $q_{Fn}$.

In particular the

$(\sigma ,v:n\to UA)$ are modal formulas

$$\mathrm{\Delta }(a_1,\dots a_n)$$

where

$\mathrm{\Delta }=\sigma$ and

$a_i=v(i)$.

The set

$\mathrm{\Sigma }$ of operations and the set

$E$ of equations constitute the presentation

$⟨{\mathrm{\Sigma }}_L,E_L⟩$ of

$L$.

Example: The variety of Boolean algebras with operator (BAO) is presented by the operations and equations of Boolean algebra plus a unary operation

$◻$ and two equations specifying that

$◻$ preserves finite meets.

Moss's coalgebraic logic

The first proposal for a logic of coalgebras parametric in the coalgebra functor

$T$ was Moss's coalgebraic logic. It can be obtained by defining

$L$ via a presentation

$$FGUA\stackrel{q_A}{⟶}LA$$

where

$G=T$. Originally, Moss's logic did not have equations, which corresponds to taking the

$q_{Fn}$ to be identities. This use of the functor

$T$ itself as a syntax constructor for a logic yields a very interesting presentation. This presentation is equivalent in expressiveness (in case

$T$ preserves weak pullbacks) to the ones we know from classical modal logic, but is quite different in terms of the opportunities it offers as a logical tool. For more see the section on Moss's Coalgebraic Logic.

The logic of all predicate liftings

Pattinson introduced predicate liftings to give a parametric treatment of coalgebraic logic that includes classical modal logic as an example. The logic of all predicate liftings can be defined in our setting in a natural way.

Remark: Note that Moss's logic is defined by applying

$T$ directly to syntax, whereas here we want to use the duality given by

$S:\mathsf{B}\mathsf{A}\to Set$ and

$P:Set\to \mathsf{B}\mathsf{A}$ to keep

$T$ on the semantic side of the duality. In fact, we might have been tempted to simply define

$L=PTS$ and while this is still the guiding idea, this direct approach is only suitable if we start from a dual equivalence of base categories such as the one given by complete atomic Boolean algebras and Set or the one given by Boolean algebras and Stone spaces. Moreover, defining

$L=PTS$ will not, in general, result in a sifted colimit preserving functor and, thus, not, in general, allow us to find a finitary presentation of

$Alg(L)$ by operations and equations.

Syntax

We define

$L=PTS$ on finitely generated free algebras:

$$LFn=PTSFn$$

We extend

$L$ to all algebras via sifted colimits (hence

$L$ preserves sifted colimits by definition).

Moreover,

$ULFn=UPTSFn$ is the set of all

$n$-ary predicate liftings:

$$\begin{array}{rl}UPTSFn& \cong UPT(2^n)\\ & =2^{T(2^n)}\\ & \cong Nat({(2^n)}^X,2^{TX})\\ & \cong Nat({(2^X)}^n,2^{TX})\end{array}$$

Since

$L$ preserves sifted colimits it has a presentation by operations and equations and this presentation presents

$L$ by all predicates liftings as

$$FGUA\stackrel{q_A}{⟶}LA$$

where

$GX=\coprod _{n\in \mathbb{N}}ULFn\times X^n$.

Semantics

The semantics

${\delta }_X:LPX\to PTX$ is given as follows.

Every

$PX$ is a sifted colimit

$c_i:Fn\to PX$. Let

$c_i^{\ast }$ be the adjoint transpose. Since

$L$ preserves sifted colimits and since

$PT{c}_i^{\ast }$ is a cocone,

${\delta }_X$ is well-defined.

In more detail,

$c_i:Fn\to PX$ is also a valuation of variable

$v:n\to UPX$ or also a tuple

$(a_1,\dots a_n)$ of subsets of

$X$. Its adjoint transpose

$X\to SFn$ combines the characteristic functions

${\chi }_i$ of all the subsets

$a_i$ into one function

$X\to 2^n$,

$x\mapsto ⟨{\chi }_1,\dots {\chi }_n⟩$. Now, given a modal operator

$\mathrm{\Delta }\in UPTSFn=2^{T(2^n)}$ we have that

$PT{c}_i^{\ast }(\mathrm{\Delta })$ is

$$TX\stackrel{T{c}_i^{\ast }}{⟶}T(2^n)\stackrel{\mathrm{\Delta }}{⟶}2$$

which, as expected, coincides with the semantics of a modal operator as a predicate lifting.

Remark: Using the Lemma above (which is special to the category

$\mathsf{B}\mathsf{A}$), we do not need to go via the finitely generated free algebras

$Fn$ and can define

${\delta }_X$ for finite

$X$ directly as the isomorphism

$$LPX=PTSPX\cong PTX$$

which, in terms of the presentation of

$L$ by modal operators, corresponds to

$$\begin{array}{rl}{\delta }_X:LPX& \to PTX\\ \mathrm{\Delta }(a_1,\dots a_n)& \mapsto \mathrm{\Delta }(a_1,\dots a_n)\end{array}$$

where

• on the left
  $\mathrm{\Delta }(a_1,\dots a_n)$ is understood as syntax, that is,
  $\mathrm{\Delta }\in UPTSFn$ and
  $(a_1,\dots a_n)\in (UPX{)}^n$ and
• on the right
  $\mathrm{\Delta }(a_1,\dots a_n)$ is evaluated by taking the predicate lifting
  $\mathrm{\Delta }$ as a function
  ${(2^X)}^n\to 2^{TX}$, that is, as a function
  $(UPX{)}^n\to UPTX$.

From Funtors to Predicate Liftings and Back

Every sifted colimit preserving functor

$L$ with a semantics

$\delta :LP\to PT$ can be represented by predicate liftings. Conversely, each set of predicate liftings presents a functor together with a semantics. We summarize this corrspondence.

Starting with a functor

$L$, its presentation

$FGU\to L$ and its semantics

$LP\to PT$, we obtain its presentation by predicate liftings in the last line, where

$\mathrm{\Delta }$ ranges over all elements of

$G_n$. Conversely, any collection of predicate liftings

$\mathrm{\Delta }$ defines a functor

$L$ obtained from "climbing the ladder up" and quotienting the corresponding

$FGUPX\to PTX$.

References

• Kurz-Rosicky: Strongly Complete Logics for Coalgebras, 2012.

Diagrams:

• Semantics of
  $L$
• From
  $L$ to
  $\mathrm{\Delta }$ (and back)