In our last installment in this series on Stone duality, we introduced the notion of Heyting algebra, which captures the basic relationships between the logical connectives “and”, “or”, and “implies”. Our discussion disclosed a fundamental relationship between distributive laws and the algebra of implication, which we put to work to discover the structure of the “internal Heyting algebra logic” of a topology.

I’d like to pause and reflect on the general technique we used to establish this relationship; like the Yoneda principle and the Principle of Duality, it comes up with striking frequency, and so it will be useful for us to give it a name. As it turns out, this particular proof technique is analogous to the way adjoints are used in linear algebra. Such analogies go all the way back to work of C. S. Peirce, who like Boole was a great pioneer in the discovery of relationships between algebra and logic. At a deeper level, similar analogies were later rediscovered in category theory, and are connected with some of the most potent ideas category theory has to offer.

Our proof that meets distribute over sups in the presence of an implication operator is an example of this technique. Here is another example of similar flavor.

Theorem: In a Heyting algebra X, the operator p \Rightarrow -: X \to X preserves any infs which happen to exist in X, for any element p \in X. [In particular, this operator is a morphism of meet-semilattices, i.e., (p \Rightarrow (q \wedge r)) = ((p \Rightarrow q) \wedge (p \Rightarrow r)), and (p \Rightarrow 1) = 1.]

Proof: Suppose that S \subseteq X has an inf, which here will be denoted \bigwedge_{s \in S} s. Then for all a \in X, we have

a \leq p \Rightarrow (\bigwedge_{s \in S} s) if and only if

a \wedge p \leq \bigwedge_{s \in S} s if and only if

(for all s \in S, a \wedge p \leq s) if and only if

for all s \in S, a \leq p \Rightarrow s.

By the defining property of inf, these logical equivalences show that p \Rightarrow (\bigwedge_{s \in S} s) is indeed the inf of the subset \{p \Rightarrow s: s \in S\}, or in other words that p \Rightarrow (\bigwedge_{s \in S} s) = \bigwedge_{s \in S} p \Rightarrow s, as desired. \Box \,

In summary, what we did in this proof is “slide” the operator p \Rightarrow - on the right of the inequality over to the operator - \wedge p on the left, then invoke the defining property of infs, and then slide back to p \Rightarrow - on the right. This sliding trick is analogous to how adjoint mappings work in linear algebra.

In fact, everything we have done so far with posets can be translated in terms of matrix algebra, provided that our matrix entries, instead of being real or complex numbers, are truth values 0, 1 (1 for “true”, 0 \mbox{ for} “false”). These truth values are added and multiplied in the way familiar from truth tables, with join playing the role of addition and meet playing the role of multiplication. In fact the lattice \mathbf{2} = \{0, 1\} is a very simple distributive lattice, and so most of the familiar arithmetic properties of addition and multiplication (associativity, commutativity, distributivity) do carry over, which is all we need to carry out the most basic aspects of matrix algebra. However, observe that 1 has no additive inverse (for here 1 + 1 = 1 \vee 1 = 1) — the type of structure we are dealing with is often called a “rig” (like a ring, but without assuming negatives). On the other hand, this lattice is, conveniently, a sup-lattice, thinking of sups as arbitrary sums, whether finitary or infinitary.

Peirce recognized that a relation can be classified by a truth-valued matrix. Take for example a binary relation on a set X, i.e., a subset R \subseteq X \times X. We can imagine each point (x, y) \in X \times X as a pixel in the plane, and highlight R by lighting up just those pixels which belong to R. This is the same as giving an (X \times X)-matrix R(\cdot, \cdot), with rows indexed by elements y and columns by elements x, where the (y, x)-entry R(y, x) is 1 (on) if (x, y) is in R, and 0 \mbox{ (off)} if not. In a similar way, any relation R \subseteq X \times Y is classified by a (Y \times X)-matrix whose entries are truth values.

As an example, the identity matrix has a 1 at the (x, y)-entry if and only if x = y. Thus the identity matrix classifies the equality relation.

A poset is a set X equipped with a binary relation R satisfying the reflexive, transitive, and antisymmetry properties. Let us translate these into matrix algebra terms. First reflexivity: it says that x = y implies (x, y) \in R. In matrix algebra terms, it says Id(y, x) \leq R(y, x), which we abbreviate in the customary way:

(Reflexivity) Id \leq R.

Now let’s look at transitivity. It says

(\exists_y (x, y) \in R and (y, z) \in R) implies (x, z) \in R.

The “and” here refers to the meet or multiplication in the rig of truth values \mathbf{2}, and the existential quantifier can be thought of as a (possibly infinitary) join or sum indexed over elements y. Thus, for each pair (x, z), the hypothesis of the implication has truth value

\sum_y R(z, y) \cdot R(y, x)

which is just the (z, x)-entry of the square of the matrix R. Therefore, transitivity can be very succinctly expressed in matrix algebra terms as the condition

(Transitivity) R^2 \leq R.

  • Remark: More generally, given a relation R \subseteq X \times Y from X to Y, and another relation S \subseteq Y \times Z from Y to Z, the relational composite S \circ R \subseteq X \times Z is defined to be the set of pairs (x, z) for which there exists y with (x, y) \in R and (y, z) \in S. But this just means that its classifying matrix is the ordinary matrix product S \cdot R!

Let’s now look at the antisymmetry condition: ((x, y) \in R and (y, x) \in R) implies x = y. The clause (y, x) \in R is the flip of (x, y) \in R; at the matrix level, this flip corresponds to taking the transpose. Thus antisymmetry can be expressed in matrix terms as

(Antisymmetry) R \wedge R^\top \leq Id

where R^\top denotes the transpose of R, and the matrix meet \wedge means we take the meet at each entry.

  • Remark: From the matrix algebra perspective, the antisymmetry axiom is less well motivated than the reflexivity and transitivity axioms. There’s a moral hiding beneath that story: from the category-theoretic perspective, the antisymmetry axiom is relatively insignificant. That is, if we view a poset as a category, then the antisymmetry condition is tantamount to the condition that isomorphic objects are equal (in the parlance, one says the category is “skeletal”) — this extra condition makes no essential difference, because isomorphic objects are essentially the same anyway. So: if we were to simply drop the antisymmetry axiom but keep the reflexivity and transitivity axioms (leading to what are called preordered sets, as opposed to partially ordered sets), then the theory of preordered sets develops exactly as the theory of partially ordered sets, except that in places where we conclude “x is equal to y” in the theory of posets, we would generally conclude “x is isomorphic to y” in the theory of preordered sets.

Preordered sets do occur in nature. For example, the set of sentences p, q, ... in a theory is preordered by the entailment relation p \vdash q (q is derivable from p in the theory). (The way one gets a poset out of this is to pass to a quotient set, by identifying sentences which are logically equivalent in the theory.)

Exercises:

  1. (For those who know some topology) Suppose X is a topological space. Given x, y \in X, define x \leq y if x belongs to the closure of y; show this is a preorder. Show this preorder is a poset precisely when X is a T_0-space.
  2. If X carries a group structure, define x \leq y for elements x, y \in X if x = y^n for some integer n; show this is a preorder. When is it a poset?

Since posets or preorders are fundamental to everything we’re doing, I’m going to reserve a special pairing notation for their classifying matrices: define

\langle x, y \rangle = 1 if and only if x \leq y.

Many of the concepts we have developed so far for posets can be succinctly expressed in terms of the pairing.

Example: The Yoneda principle (together with its dual) is simply the statement that if X is a poset, then x = y if and only if \langle -, x \rangle = \langle -, y \rangle (as functionals valued in \mathbf{2}) if and only if \langle x, - \rangle = \langle y, - \rangle.

Example: A mapping from a poset (X, \langle, \rangle_X) to a poset (Y, \langle, \rangle_Y) is a function f: X \to Y such that \langle x, y \rangle_X \leq \langle f(x), f(y) \rangle_Y.

Example: If X is a poset, its dual or opposite X^{op} has the same elements but the opposite order, i.e., \langle x, y \rangle_X = \langle y, x \rangle_{X^{op}}. The principle of duality says that the opposite of a poset is a poset. This can be (re)proved by invoking formal properties of matrix transpose, e.g., if R^2 \leq R, then (R^\top)^2 = (R^2)^\top \leq R^\top.

By far the most significant concept that can be expressed in terms of these pairings that of adjoint mappings:

Definition: Let X, Y be posets [or preorders], and f: X \to Y, g: Y \to X be poset mappings. We say (f, g) is an adjoint pair (with f the left adjoint of g, and g the right adjoint of f) if

\langle f(x), y \rangle_Y = \langle x, g(y) \rangle_X

or, in other words, if f(x) \leq y if and only if x \leq g(y). We write f \dashv g. Notice that the concept of left adjoint is dual to the concept of right adjoint (N.B.: they are not the same, because clearly the pairing \langle x, y \rangle is not generally symmetric in x and y).

Here are some examples which illustrate the ubiquity of this concept:

  1. Let X be a poset. Let X \times X be the poset where (x, y) \leq (x', y') iff (x \leq x' and y \leq y'). There is an obvious poset mapping \delta: X \to X \times X, the diagonal mapping, which takes x to (x, x). Then a meet operation \wedge: X \times X \to X is precisely a right adjoint to the diagonal mapping. Indeed, it says that (a, a) \leq (x, y) if and only if a \leq x \wedge y.
  2. Dually, a join operation \vee: X \times X \to X is precisely a left adjoint to the diagonal mapping \delta: X \to X \times X.
  3. More generally, for any set S, there is a diagonal map \Delta: X \to X^S which maps x \in X to the S-tuple (\ldots, x, x, x, \ldots). Its right adjoint X^S \to X, if one exists, sends an S-tuple (x_s)_{s \in S} to the inf of the set \{x_s: s \in S\}. Its left adjoint would send the tuple to the sup of that set.
  4. If X is a Heyting algebra, then for each x \in X, the conjunction operator x \wedge -: X \to X is left adjoint to the implication operator x \Rightarrow -: X \to X.
  5. If X is a sup-lattice, then the operator \sup: PX \to X which sends a subset S \subseteq X to \sup(S) \in X is left adjoint to the Dedekind embedding i: X \to PX. Indeed, we have \sup(S) \leq a if and only if (for all s \in S, s \leq a) if and only if S \subseteq \{x \in X: x \leq a\} = i(a).

As items 1, 2, and 4 indicate, the rules for how the propositional connectives \wedge, \vee, \Rightarrow operate are governed by adjoint pairs. This gives some evidence for Lawvere’s great insight that all rules of inference in logic are expressed by interlocking pairs of adjoint mappings.

Proposition: If f \dashv g and f' \dashv g' where g: X \to Y and g': Y \to Z are composable mappings, then f \circ f' \dashv g' \circ g.

Proof: \langle f f' z, x \rangle_X = \langle f' z, g x \rangle_Y = \langle z, g' g x \rangle_Z. Notice that the statement is analogous to the usual rule (A B)^\dagger = B^\dagger A^\dagger, where A^\dagger refers to taking an adjoint with respect to given inner product forms.

We can use this proposition to give slick proofs of some results we’ve seen. For example, to prove that Heyting algebras are distributive lattices, i.e., that p \wedge (x \vee y) = (p \wedge x) \vee (p \wedge y), just take left adjoints on both sides of the tautology \delta \circ g = (g \times g) \circ \delta, where g = p \Rightarrow - is right adjoint to p \wedge -. The left adjoint of the left side of the tautology is (by the proposition) p \wedge - applied to \vee. The left adjoint of the right side is \vee applied to (p \wedge -) \times (p \wedge -). The conclusion follows.

Much more generally, we have the

Theorem: Right adjoints g: X \to Y preserve any infs which exist in X. Dually, left adjoints f: Y \to X preserve any sups which exist in Y.

Proof: \langle y, g(\bigwedge_{s \in S} x_s) \rangle_Y = \langle f(y), \bigwedge_{s \in S} x_s \rangle_X = \bigwedge_{s \in S} \langle f(y), x_s \rangle_X where the last inf is interpreted in the inf-lattice \mathbf{2}. This equals \bigwedge_{s \in S} \langle y, g(x_s) \rangle_Y. This completes the proof of the first statement (why?). The second follows from duality.

Exercise: If X is a Heyting algebra, then there is a poset mapping - \Rightarrow c: X^{op} \to X for any element c. Describe the left adjoint of this mapping. Conclude that this mapping takes infs in X^{op} (i.e., sups in X) to the corresponding infs in X.