---
tags: logic, category theory, stone duality, sri pranav kunda
---

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

# A Short Introduction to Stone Duality (Logic)

(under construction ... let me know about typos and any other questions)

In Part 1 we studied the [algebra of sets](https://en.wikipedia.org/wiki/Algebra_of_sets). In Part 2, we abstracted from the fact that sets have elements and moved from [fields of sets](https://en.wikipedia.org/wiki/Field_of_sets) to [lattices](https://en.wikipedia.org/wiki/Lattice_(order)) and [Boolean algebras](https://en.wikipedia.org/wiki/Boolean_algebra). In particular, we have seen that any finite Boolean algebra can be represented as a field of sets.

In this part, we look at the same material from the point of view of logic. The study of classical propositional logic (CPL) is closely related to the study of Boolean algebra. For example, we will see that the representation theorem of Boolean algebra (every Boolean algebra is isomorphic to a field of sets) leads to an important theorem of logic, namely the completeness of CPL.

On the way, we explain the notion of free algebra which will also play an important role when we generalise the representation theorem to infinite Boolean algebra (Stone's theorem).

Finally, let me emphasize that the methods we learn in this section play a role in many areas of mathematics and are not limited to the study of logics.

## Introduction

A fundamenal concept in logic is the distinction of syntax and semantics. We will see later that this distinction is related to the duality between (finite) Boolean algebras and (finite) sets. Roughly speaking, one can say that syntax lives on the side of algebra and semantics lives on the side of sets.

In slightly more detail, on the syntactic/algebraic side, we have rules for deriving equations. It is easy to check whether a given derivation follows the rules. But a problem with rules is: How do we know that we found the right rules? Is there a way to justify the rules?

To justifity the rules we need to step outside of syntax and seek to explain its meaning independently.

In our setting, we will explain the meaning of classical propositional logic (CPL) using a set-theoretic semantics, , in other words, Venn diagrams. Venn diagrams enforce certain equations on the logic. For example, we can use Venn diagrams to prove that $\neg\neg A=A$ or that $\neg(A\wedge B)=\neg A\vee \neg B$.

After setting out the semantics, we can ask whether the rules (that is, the axioms of Boolean algebra) match up with the semantics. This leads to two questions:

**Soundness** of CPL: Do all equations of Boolean algebra hold in the interpretation of Venn Diagrams?

**Completeness** of CPL: Can we derive all equations that are true in all Venn diagrams from the axioms of Boolean algebra?

We are going to prove that CPL is sound and complete.

## Syntax

**Definition:** The set $Term(P)$ of 'propositional formulas' or 'Boolean terms' of CPL over a set $P$ of 'propositional variables' or 'atomic propositions' is the smallest set of formulas containing the constant $0,1$ and that is closed under the unary operation $\neg$ ('negagion') and the two binary operations $\wedge$ ('and', 'conjunction', 'meet') and ('or, 'disjunction', 'join'). The 'insertion of generators'
$$\eta':P\to Term(P)$$

is defined by $\eta'(p)=p$ for all $p\in P$.

**Remark:** By definition, $Term(P)$ is an algebra wrt the operations $(0,1,\neg,\wedge,\vee)$ but at the moment we have not imposed any equations.

The most important property of the term-algebra is that one can define functions on $Term(P)$ by recursion on the structure of terms. The details are given in the next proposition.

**Proposition (universal property of the term-algebra):** Let $A$ be an algebra that interprets the operations $(0,1,\neg,\wedge,\vee)$. Then for any $s:P\to A$ the function $s^\ast : Term(P)\to A$ defined by [^interpretationA]
\begin{align}
s^\ast(p)&=s(p)\\
s^\ast(0)&=0^A\\
s^\ast(1)&=1^A\\
s^\ast(\neg t)&=\neg^A s^\ast(t)\\
s^\ast(t\wedge t')&=s^\ast(t)\wedge^A s^\ast(t')\\
s^\ast(t\vee t')&=s^\ast(t)\vee^A s^\ast(t')
\end{align}

is the unique $(0,1,\neg,\wedge,\vee)$-morphism such that $s^\ast\circ \eta'=s$.

[^interpretationA]: We write $0^A$ (etc) for the interpretation of $0$ in $A$ (etc). To make the equations easier to read it is common to drop the superscripts, but it is important to clearly understand the distinction between the syntactic operation symbols (such as $\wedge$) and their semantic interpretation as functions (such as $\wedge^A: A\times A \to A$).

In the same way as we learn computing with numbers by applying certain equations, we now lay out the equations of logical reasoning with CPL.

In fact, I dont write them out here, they are just the equations of [Boolean algebra](https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Definition).

**Definition:** For Boolean terms $\phi,\psi\in Term(P)$, we write
$$\vdash \phi\approx\psi$$

if the equation $\phi\approx\psi$ can be derived from the axioms of Boolean algebra and the rules of equational logic which we summarize below.

**Notation (writing $\approx$ instead of $=$):** Why do we write now "$\approx$" instead of "$=$"? Since we started to study logic using mathematical methods, logic now apppears on two different levels, the object-level and the meta-level. On the meta-level we use math (hence logic) as usual. On the object level, the logic we study is CPL. For example, we use the word "and" on the meta-level and the symbol $\wedge$ on the object level. Similarly, when reasoning in CPL (or in Boolean algebra), we will use from now on "$\approx$" and continue to use "$=$" in the sense of mathmatics.

(Watch out: I may slip back into sloppy habits and write "$=$" where it should be "$\approx$".)

**Definition:** The rules of **equational logic** are
$$
\frac{}{t\approx t}{\ \rm (refl)\ }
\quad\quad\quad\quad
\frac{t_1\approx t_2}{t_2\approx t_1}{\ \rm (sym)\ }
\quad\quad\quad\quad
\frac{t_1\approx t_2\quad\quad t_2\approx t_3}{t_1\approx t_3}{\ \rm (trans)\ }
$$
and for all $n$-ary operations $\sigma$
$$
\frac{t_1\approx t_1'\quad\quad \ldots \quad\quad t_n\approx t_n'}{\sigma(t_1, \ldots t_n) \approx \sigma(t_1',\ldots t_n')}{\ \rm (cong)\ }
$$
as well as a rule for applying a substitution $s:P\to Term(P)$
$$
\frac{t\approx t'}{s^\ast(t) \approx s^\ast(t')}{\ \rm (subst)\ }
$$

where $s^\ast$ was defined above.

## Semantics

We now define formally what it means to interprete propositional logic via Venn diagrams.

For this we fix a (finite) set $X$. Atomic propositions $p\in P$ will be mapped to subsets of $X$. And we define the semantics of CPL so that $0$ is the empty set, $1$ is $X$, $\neg$ is complement, $\wedge$ is intersection, $\vee$ is union.

Write $\mathcal P X$ for the set of subsets of $X$. $\mathcal PX$ is the so-called powerset of $X$.

To get the interpretation off the ground, we need an interpretation $v:P\to\mathcal PX$ of the propositional variables ($v$ to remind us of 'valuation').

**Definition:** (Set Theoretic Semantics) Let $X$ be a set and $v:P\to\mathcal PX$. Then the interpretation of CPL formulas is given as follows.
\begin{align}
\sem{p}_v &= v(p)\\
\sem{\neg\phi}_v &= X\setminus\sem{\phi}_v\\
\sem{\phi\wedge\psi}_v &= \sem{\phi}_v\cap\sem{\psi}_v\\
\sem{\phi\vee\psi}_v &= \sem{\phi}_v\cup\sem{\psi}_v\\
\end{align}
The function $\sem{-}:Term(P)\to\mathcal PX$ is known as the semantics of CPL (wrt to the valuation $v$) or also as sometimes as meaning function.

**Definition:** A CPL-formula $\phi$ is called a **tautology** if $\sem{\phi}_v=X$ for all valuations $v$.

**Definition:** We define
$$\models\phi\approx\psi \ \ \Longleftrightarrow \ \ \forall v:P\to \mathcal PX\,.\,\sem{\phi}_v = \sem{\psi}_v$$

If $\models\phi\approx\psi$ we say that the equation is valid.

With the help of Venn diagrams one can prove that the equations of Boolean algebra are valid:

**Proposition (soundness of CPL):** $\quad\vdash \phi\approx\psi \ \Longrightarrow \ \models\phi\approx\psi$.

Our next aim is to show completeness, which is the converse of soundnes. Completeness entails that if an equation is valid, then it can be derived by equational reasoning from the axioms of Boolean algebra.

The first step in the completeness proof is to show that the semantics is a homomorphism of Boolean algebras. The second step is to use Stone duality to represent every Boolean algebra as a Boolean algebra of subsets.

## Algebraic Semantics

We have seen that we can represent the formulas of CPL over propositional variables $P$ as elements of the $(0,1,\neg,\wedge,\vee)$-algebra $Term(P)$. But $Term(P)$ is not a Boolean algebra because it does not satisfy the equations of Boolean algebra.

The term-algebra $Term(P)$ is also called the absolutely free algebra to express the idea that no equations at all are enforced.

In the following we will show how to construct from $Term(P)$ the free Boolean algebra, which is obtained from $Term(P)$ by only enforcing the axioms of Boolean algebra but not more.

### The Free Boolean Algebra

Recall the following.
1. The set $Term(P)$ of Boolean terms is the set of all terms in that can be formed from the set $P$, the constants $0,1$, the unary operation $\neg$ and the two binary operations $\wedge$ and $\vee$.
2. $\eta'_P:P\to Term(P)$ is the function that includes the variables in the terms.
3. For any function $f:P\to B$ into a Boolean algebra $B$, there is a unique $(0,1,\neg,\wedge,\vee)$-morphism $f^\ast:Term(X)\to B$ such that $f^\ast\circ \eta'=f$.

We now define the free Boolean algebra $FP$ over a set $P$.

**Definition:** Let $FP$ be the set of equivalence classes $[\phi]$ where $\phi$ is Boolean term and $[\phi]=\{\psi \in Term(P) \ {\mid}\, \vdash \phi\approx\psi\}$. The map $\eta:P\to FP$ is defined by $p\mapsto [p]$.

The key ingredient in the proof of the next proposition is that equational logic satisfies the congruence rule (see above).

**Proposition:** $FP$ is a Boolean algebra.

The next proposition shows that not only the term-algebras but also the free Boolean algebras enjoy a universal property.

Given a Boolean algebra, we write $UB$ for the set of elements of $B$. While it is common to not distinguish notationally between an algebra and its sets of elements, we will see later why, in the context of the next proposition, it pays to make explicit the operation $U$ that takes an algebra to its underlying set. Similarly, we distinguish between a Boolean algebra morphism $g:B\to B'$ and its underlying function $Ug:UB\to UB'$.

**Proposition (universal property of the free Boolean algebra):** For all Boolean algebras $B$ and all maps $f:P\to UB$, there is a unique Boolean algebra morphism $f^\sharp:FP\to B$ such that $Uf^\sharp\circ \eta=f$.

To summarize, we have now a Boolean algebra, $FP$, that represents the essence of the syntax of CPL, both formulas and axioms.

The next proposition shows that we can also represent the semantics of CPL as a Boolean algebra.

**Proposition:** $\mathcal PX$ is a Boolean algebra when interpreting $(0,1,\neg,\wedge,\vee)$ as $(\emptyset, X,(-)^c,\cap,\cup)$.

So now we represented both syntax and semantics as algebras, we can aim at proving completeness using algebraic methods.

But before we go there, we prepare the ground by investigating a particular Boolean algebra, namely $2^{2^P}$.

On the way, we are going to practice a very useful skill, namely to switch between the two different views of propositions-as-sets and propositions-as-functions.

---

(the following is being written ... dont read yet)

## Propositions-as-sets and Propositions-as-functions

The purpose of this subsection is to investigate the Boolean algebra $2^{2^P}$ for some finite set $P$.

We switch between the propositions-as-sets view (relying on the operations $\cap$, $\cup$, $(-)^c$ on $2^X$) and the propositions-as-functions view (relying on the operations $\wedge$, $\vee$, $\neg$ on the Boolean algebra $2$).

For example, $\eta_P:P\to 2^{2^P}$ (we may drop the subscript) is defined by $\eta(x)=\{a\in 2^X \mid x\in a\}$ or also by $\eta(x)(a)=a(x)$. In the first case, $\eta(x)$ is a set of subsets of $X$, in the second case $\eta(x)$ is a function $2^P\to 2$.

**Definition:** Define $\star: 2\times 2\to 2$ via $1\star q=q$ and $0\star q=\neg q$.

In other words, $p\star q=1$ iff $p=q$. This definition is of interest because of the following.

**Proposition:** Let $a,b\in 2^P$. Then $a=b$ if and only if $\bigwedge_{x\in P} a(x)\star\eta(x)(b) = 1$

**Remark:** Translating from propositions-as-functions to the propositions-as-sets $\bigwedge_{x\in X} a(x)\star\eta(x)$ becomes $\{a\}$.

The proposition allows us to rewrite any $t\in2^{2^P}$ as a join of meet of generators:

**Lemma:** Every element $t\in 2^{2^P}$ can be written as [^scope]
$$t=\bigvee_{a\in t} \bigwedge_{x\in P} a(x)\star\eta(x)$$

[^scope]: The scope of $\bigvee$ and $\bigwedge$ extens as far to the right as possible. For example, $\bigvee_{a\in t} \bigwedge_{x\in X} a(x)\star\eta(x)$ is short for $\bigvee_{a\in t} \left( \bigwedge_{x\in X} \left( a(x)\star\eta(x)\right)\right)$.

**Remark:** If we switch from the propositions-as-functions to the propositions-as-sets presentation the equation of the lemma becomes
\begin{align}
t = \bigcup \left\{\bigcap\{\eta(x) \mid x\in a\}\cap\bigcap\{\eta(x)^c\mid x\notin a\} \ \mid \ a \in t \right\}.
\end{align}

The equation from the lemma is nothing but the familiar [disjunctive normal form](https://en.wikipedia.org/wiki/Disjunctive_normal_form). Let us look at an example.

**Example:** Let $P=\{p,q\}$ and $t$ be the truth-table of $\star$. Then $t=\bigvee_{a\in t} \bigwedge_{x\in P} a(x)\star\eta(x)$ is just another notation for $p\star q = (p\wedge q) \vee (\neg p\vee\neg q)$.[^tstar]

[^tstar]: Note that $a$ ranges over the two rows of the truth-table that evaluate to $1$. Also recall that if $a(x)=0$ then $a(x)\star p=\neg p$.

...

## Completeness

We show how completeness follows from $FP\cong 2^{2^P}$ ...

...

## Proving Completeness

Three different completenss proofs:
- $2^{2^P}$ has the universal property of a free Boolean algebra
- $2^{2^P}$ is a retract of $Term(P)$
- Using duality

To be continued ...

<!--## Background

Some background on logic: Aristotle[^Aristotle], Boole, Frege, Russell, Goedel ... the zoo of logics in computer science ...
-->