$\newcommand{\sem}[1]{[\![#1]\!]}$

# Canonical Extensions of Boolean Algebras with Operators

Let $B$ be a Boolean algebra with a finite-meet preserving modal operator $\Box:B\to B$.

Every Boolean algebra $B$ is the algebra of subsets of a set $X$, which can be defined as the set of maximal consistent theories, or ultrafilters, of $B$. [^ultrafilter] We write
$$\sem - : B\to PX $$

for the embedding [^Stone] defined by
$$x\in\sem b \ \stackrel{\rm def}\Longleftrightarrow b\in x.$$

$PX$ is also known as the **canonical extension** of $B$, in particular in the situation where $B$ has been expanded by additional modal operators (and $PX$ by the corresponding relations).

**Notation 1:** The logical interpretation of the representation theorem is given by
$$x\Vdash b \ \stackrel{\rm def}\Longleftrightarrow \ b\in x.$$

Intuitively, the world $x$ satisfies $b$ (or forces $b$) iff $b$ is in the theory of $x$.

**Aim:** This note explains how to extend this relationship between sets/spaces and algebras to relational structures and Boolean algebras with operators.

For this purpose, we need to construct a Boolean algebra with operator (BAO) for each Kripke frame and, vice versa, a Kripke frame for each BAO.

## The Complex Algebra of an ordered Kripke Frame

We show how to construct a BAO from a Kripke frame.

**Definition 1:** Given a Kripke frame[^kripkeframe] $(X,R)$, one defines the modal operator, or predicate transformer, $\Box:PX\to PX$ as
$$ \Box a \ \stackrel {\rm def} = \ \{x\in X\mid \forall y\in X\,.xRy \Rightarrow y\in a\}.$$

Intuitively, $\Box a$ holds in $x$ iff $a$ holds in all successors of $x$.

**Exercise:** Show that $\Box$ preserves intersections.

To summarise, every Kripke frame gives rise to a Boolean algebra with operator. This algebra is also known as the **complex algebra** of the Kripke frame.

Conversely, given a BAO, can we always represent it as a subalgebra of the complex algebra of a Kripke frame?

## The Canonical Frame of a BAO

Given a BAO $(B,\Box)$, how do we find a relation $R$ representing $\Box$?

**Definition 2:** Given $\Box:B\to B$, we define $R$ on the set $X$ of ultrafilters of $B$ as
$$xR y \quad \stackrel{\rm def}\Longleftrightarrow \quad \forall b\in B\,. \Box b\in x \Rightarrow b\in y.$$

Below, we will show that the $\Box:PX\to PX$ induced by $R$ (see Def.1) agrees with the original $\Box:B\to B$. The key to proving this is the

**Truth Lemma:** $\quad \Box b\in x \ \Longleftrightarrow \ \forall y\in X\,.xR y \Rightarrow b\in y$

*Proof:* "$\Rightarrow$" is immediate from the definition of $R$. For "$\Leftarrow$", assume $\forall y\in X\,. xRy \Rightarrow b\in y$ and, for a contradiction, $\Box b\notin x$.[^contradiction] Let $F=\{c\in B \mid \Box c\in x\}.$ If $F$ is not consistent, that is, if $0\in F$, then $\Box 0\in x$, hence $\Box b\in x$ (by monotonicity of $\Box$), contradicting $\Box b\notin x$. Otherwise $F$ is consistent and we will show that there is an ultrafilter $y$ containing $F\cup\{\neg b\}$. First note that $F$ is closed under finite meets because $\Box$ preserves them. Moreover, $\neg b\wedge c$ is consistent for all $c\in F$. To show this, suppose $\neg b\wedge c = 0$, hence $c\le b$, hence $\Box c\le \Box b$. Now $\Box c\in x$ implies $\Box b\in x$, contradicting $\Box b\notin x$. This shows that $F\cup\{\neg b\}$ is contained in some ultrafilter $y$. We have $xRy$ by definiton of $R$, hence $b\in y$, contradicting $F\cup\{\neg b\}\subseteq y$. Q.E.D.

$R$ now induces an operation $\Box :PX\to PX$:

**Remark 2:** Following Def.1, the relation $R$ induces an operation $\Box :PX\to PX$
$$ \Box a \ \stackrel{\rm def}= \ \{x\in X\mid \forall y\,.xR y \Rightarrow y\in a\}.$$

The next theorem shows that every BAO has a canonical extension:

**Jonsson-Tarski Represenation Theorem:** Every BAO is a subalgebra of a complex algebra.

*Proof:* We have to show that $\sem- : B\to PX$ is a morphism of BAOs. We know that it is a Boolean algebra morphism from Stone's representation theorem. It remains to show that $\sem-$ preserves $\Box$, that is,
\begin{align}
\sem{\Box b} & = \{x \mid \Box b \in x\} \\
& = \{x \mid \forall y\,.xR y \Rightarrow b\in y\} \\
& = \{x \mid \forall y\,.xR y \Rightarrow y\in\sem b\} \\
& = \Box \sem b \\
\end{align}
where the first and third equation are due to the definition of $\sem-$, the fourth equation is the definition of $\Box$ in Remark 2 and the second equation is the truth lemma. Q.E.D.

**Remark:** $R$ is the largest relation satisfying $\ \Box b\in x \ \Longrightarrow \ \forall y\in X\,.xR y \Rightarrow b\in y.$ [^largestrel]

## A Coalgebraic Jonsson-Tarski Theorem

The move from Stone's representation theorem to the Jonsson-Tarski representation theorem can be seen as extending the former by two functors, one on spaces and one on algebras.

One can generalise this then as follows.

- A finitely complete and cocomplete category $\cal C$ (generalising finite Boolean algebras). This works well for example in the case where finitely generated free algebras are finite.
- A functor $L$ on $\cal C$ (generalising the modal algebra functor on finite Boolean algebras).

One then obtains a generalisation of the Jonsson-Tarski theorem representing $L$-algebras on the Ind-completion of $\cal C$ by $L^{op}$-coalgebras on the Ind-completion of $\cal C^{op}$ (= algebras on the Pro-completion of $\cal C$).

## References

For the Jonsson-Tarski theorem, I consulted

- Jonsson and Tarski: [Boolean Algebras with Operators](https://www.jstor.org/stable/2372123). 1951. (Def 2.13, Thm 2.15)
- Blackburn, de Rijke, Venema: [Modal Logic](https://www.cambridge.org/core/books/modal-logic/F7CDB0A265026BF05EAD1091A47FCF5B). (Thm 5.43)

The coalgebraic generalisation is in
- Kurz and Rosicky. [Strongly complete logics for coalgebras](https://alexhkurz.github.io/papers/KR/strcompl.pdf). 2012.

[^ultrafilter]: Ultrafilters on $B$ are in one-to-one correspondence with Boolean algebra homomorphism $B\to 2$. In detail, $x\subseteq B$ is an ultrafilter if $x$ is an upset closed under conjunctions. Moreover an ultrafilter is maximal in the sense that for all $b\in B$ either $b$ or $\neg b$ is in $x$ and an ultrafilter is consistent meaning that $0\notin x$.

[^Stone]: That the embedding is a Boolean algebra morphism is straightfoward to check. The only tricky part is, for infinite BAs, that the embedding is injective. This depends on Zorn's lemma and, therefore, on the axiom of choice.

[^kripkeframe]: A Kripke frame is a set $X$ with a relation $R\subseteq X\times X$.

[^contradiction]: Intuitively, $\Box b\notin x$ means that there is a successor $y$ of $x$ such that $\neg b$ holds in $y$. The main step of the proof is to construct such a $y$. Btw, this proof is a nice illustration of [Cantor's paradise](https://en.wikipedia.org/wiki/Cantor%27s_paradise): For a mathematical object to exist it is enough that its existence does not lead to a contradiction with the rest of mathematics. In our case, we will use this idea to prove the existence of $y$ based on the principle that every consistent theory is contained in a maximal consistent one.

[^largestrel]: That $R$ satisfies the condition was the easy direction of the truth lemma. Now let $R'$ be another relation satisfying $\ \Box b\in x \ \Longrightarrow \ \forall y\in X\,.xR' y \Rightarrow b\in y.$ Assume $(x,y)\notin R$, that is, $\exists b\in B\,.\Box b\in x \ \& \ b\notin y.$ It follows that not $xR'y$.