First-Order Categorical Logic 3

Prev TOC Next

JB: Okay, let’s talk more about how to do first-order classical logic using some category theory. We’ve already got the scaffolding set up: we’re looking at functors

$B \colon \textrm{FinSet} \to \textrm{BoolAlg}.$

You can think of $B(S)$ as a set of predicates whose free variables are chosen from the set S. The fact that B is a functor captures our ability to substitute variables, or in other words rename them.

But now we want to get existential and universal quantifiers into the game. And we do this using a great idea of Lawvere: quantifiers are adjoints to substitution.

To understand this, first notice that a Boolean algebra is a special case of a partially ordered set, or poset for short: if P, Q are two elements of our Boolean algebra and P implies Q, we can write $P \le Q$ , and this $\le$ is a partial order: it’s reflexive, transitive and antisymmetric.

Second, notice that a poset is a special case of a category. Given a poset, we get a category whose objects are the elements of our poset, there exists a unique morphism from P to Q if $P \le Q$ , and there is no morphism from P to Q otherwise.

We could digress and say exactly which categories come from posets this way, and then exactly which categories come from Boolean algebras. If this were a course on category theory I’d do it. But we don’t need this now, so I won’t: if you care, you can look it up by clicking on some of the links I’ve offered. Let’s plunge ahead.

Given two categories C and D, we can talk about things called functors $F \colon C \to D$ . In fact we’ve already been talking about them! But when C and D are posets, a functor $F \colon C \to D$ boils down to something simple, namely the usual sort of map between posets, a monotone map, meaning a function such that

$c \le c' \textrm{ implies } F(c) \le F(c)'.$

In particular, any homomorphism of Boolean algebras is a monotone map, so we can think of it as a functor.

Are you with me? We’ve got functors running all over the place now. We’ve got a functor

$B \colon \textrm{FinSet} \to \textrm{BoolAlg}$

so for any function $f \colon S \to T$ we get a homomorphism of Boolean algebras

$B(f) \colon B(S) \to B(T).$

But now we’ve revealed that $B(f)$ is itself a functor! Okay? I want to start doing things with this functor, but I can’t tell if I’m going too fast or too slow.

MW: Just right! Let’s look at a special case, just to make sure.

Category theorists like to use n to stand for their favorite n-element set. Let 2 stand for the set {x,y}, so 2 is an object in FinSet. Let 3 be {x,y,z}. Hmm, I want to think about our two chief examples of Boolean algebras: (a) equivalence classes of formulas; (b) relations in a structure. That would mean we have two functors from FinSet to BoolAlg, say B_form and B_rel. For the moment let B = B_form. And just to be really specific, let’s say our theory is DLO, dense linear orderings without endpoints. (When we get to B_rel, we’ll look at $\mathbb{Q}$ .)

So B(2) is the set of things like [x<y] and [¬x=y] and even [∃z(x<z<y)], where the brackets mean “equivalence class”. Thus [x<y] and [∃z(x<z<y)] are the same, since DLO proves that the two formulas are equivalent. Also x<y implies ¬x=y, which means that [x<y]≤[¬x=y].

B(3) contains things like [x<z<y]. Let’s look at two morphisms in FinSet: f:{x,y}→{x,y,z} and g:{x,y,z}→{x,y}. I’ll let f be the obvious inclusion map, while g is a surjection; we’ll decide later which one.

B(f) maps B(2) to B(3). A class like [x<y] gets sent to an equivalence class of formulas with the three free variables x,y, and z. Now we could be really cool and pretend that z is present in x<y. (“There it is, don’t you see it? Do you need a new pair of glasses?”) Or we could take pity on the reader, and note that $[x\!<\!y \wedge z=z]$ is logically equivalent to x<y.

You want me to notice that B(2) and B(3) are both categories, of a rather particular kind; also B(f), as a Boolean algebra homomorphism, is a functor between these categories.

OK, full steam ahead!

JB: Thanks for bringing up both flavors of example: the more syntactic examples where each Boolean algebra $B(n)$ consists of equivalence classes of formulas, and the more semantic examples where $B(n)$ is some Boolean algebra of subsets of $V^n$ for some set $V.$ It’s good to gain intuition from both.

Full steam ahead! If you’ve got a functor $L \colon C \to D$ between categories, a right adjoint of $L$ is a functor going back, $R \colon D \to C$ , such that there’s a natural isomorphism

$\textrm{hom}(Lc,d) \cong \textrm{hom}(c,Rd)$

for all $c \in C, d \in D.$ This means there’s a natural one-to-one correspondence between morphisms $f \colon Lc \to d$ and morphisms $g \colon c \to Rd.$

Luckily, we don’t need to think about what ‘natural’ means when C and D are posets, which is the case we care about now. When a category is a poset, there’s at most one morphism from any object to any other. So when C and D are posets, saying there’s a natural one-to-correspondence between morphisms $f \colon Lc \to d$ and morphisms $g \colon c \to Rd$ is just saying

There is a morphism $f \colon Lc \to d$ iff there is a morphism $g \colon c \to Rd$ .

But remember: in a poset we denote the existence of a morphism by ≤. So, we’re just saying

$Lc \le d$ iff $c \le Rd$ .

And remember, L and R, being functors between mere posets, are called ‘monotone maps’.

Okay, now let’s do something serious. Let’s take a functor

$B \colon \textrm{FinSet} \to \textrm{BoolAlg}$

and suppose that for each function $f \colon S \to T$ , the monotone map

$B(f) \colon B(S) \to B(T)$

has a right adjoint! Let’s see what this does for us.

Let’s start by looking at a function f that’s not surjective. The most important non-surjective function is the unique function from the empty set to a 1-element set. But this is case is confusingly simple, so let’s try a function from a 1-element set to a 2-element set. Let’s take the function

$f \colon \{x\} \to \{x,y\}$

sending x to itself.

And let’s suppose our Boolean algebra consists of equivalence classes of formulas, like you were considering. But I won’t keep keep saying ‘equivalence’ classes”, because it gets tiresome; I’ll just call these equivalence classes ‘predicates’ if you don’t mind. We’ve already seen that

$B(f) \colon B(\{x\}) \to B(\{x,y\})$

sends any predicate in the variable x to the same predicate thought of as a predicate in the variables x and y. So, it doesn’t do much, at least not visibly.

But now let’s suppose $B(f)$ has a right adjoint! This right adjoint will turn any predicate $G(x,y)$ in the variables x and y into some predicate $H(x)$ in just the variable x.

How? What is $H(x)$ ? We can figure it out!

By the definition of right adjoint we know that

$P(x) \le G(x,y)$ iff $P(x) \le H(x)$

for any predicate $P(x)$ in $B(\{x\})$ . Note at left $P(x)$ is being thought of as a predicate in in the variables x and y: we have silently applied $B(f)$ to it. Luckily, only pedants need care.

Can you figure out what $H(x)$ must be?

MW: Universal quantification. That is, $H(x)\equiv\forall y G(x,y)$ . If P(x) implies G(x,y) regardless of the value of y, then P(x) implies $\forall y G(x,y)$ , and vice versa.

This also makes sense if you think about relations, i.e., B_rel. Here B(f) propagates truth-values up along the y-axis, so B(f) applied to P results in a bunch of columns entirely true or entirely false. (This must be where Tarski’s term “cylindric algebra” originates.) This columnized P is a subset of G if and only if the original P is a subset of what you get by squashing G flat, using the rule that all points in a G-column must be true for the squashed-flat point (under the column) to be true.

So of course the left adjoint must be existential quantification. Now we want

$G(x,y)\leq P(x)$ iff $\exists y G(x,y)\leq P(x)$

Thinking about B_rel makes this obvious: just change the “squashing” rule to make the point under the column true if a single point in the column is true. From the standpoint of B_form, this fits right in with an inference rule sometimes found in formal treatments of predicate logic: from $\exists y G(x,y)$ , infer G(x,c), where c is a newly introduced constant. (Of course we see this mode of reasoning all the time in regular mathematics: “By the lemma, there is a weakly socratic number larger than x, let’s call it c.”)

OK, guess it’s time to look at a surjection, say g:{x,y}→{x}.

JB: Okay. But first let me pound the pulpit and loudly repeat the moral: universal quantifiers are right adjoints, existential quantifiers are left adjoints. In words:

$P(x)$ implies $G(x,y)$
iff
$P(x)$ implies $\forall y \, G(x,y)$

and

$G(x,y)$ implies $P(x)$
iff
$\exists y \, G(x,y)$ implies $P(x)$ .

I can imagine nonexperts in logic being freaked out by these rules, because of how the variable y switches from being free to bound, so I should assure them that this is ordinary classical logic, not some weird category-theorist’s version. It might help them to imagine an implicit universal quantifier in front of all unbound variables, so if I just walk up to you and blurt out “G(x,y) implies P(x),” I mean this is true for all x and all y. It’s clear then that this is equivalent to saying “∃y G(x,y) implies P(x)”.

It might also help to think of P and G as functions taking values in the poset of truth values, $\{\bot, \top\}$ , and restate the above rules as

$P(x) \le G(x,y)$ iff $P(x) \le \inf_y G(x,y)$

and

$G(x,y) \le P(x)$ iff $\sup_y G(x,y) \le P(x)$

Again, when I say $P(x) \le G(x,y)$ , what I mean is that this is true for all x and all y.

This is what you were getting at when you spoke of “propagating truth-values up along the y-axis” and the like. We can think of P as a vector of truth values, and G as a matrix of truth values. We can turn P into a matrix that’s constant on columns by treating P(x) as a function of x and y that happens to not depend on y. On the other hand, we can turn G into a vector in two ways. The left adjoint way gives the vector ∃y G(x,y), while right adjoint way gives ∀y G(x,y).

You recalled two kinds of functors B: FinSet → BoolAlg: the ‘syntactic’ kind B_form, and the ‘semantic’ kind B_rel. This makes me want to emphasize that there’s not a big difference between these examples: the main difference is our attitude towards them, and our terminology.

For example, let’s take the ‘semantic’ example I’ve just been discussing, where

$B_{\textrm{rel}}(n) = P(V^n)$

for some set $V$ . We can also think of this example more ‘syntactically’. We can make up a language with one n-ary formula for each element of B_rel(n), and define all the Boolean operations on these formulas in the obvious way, e.g. by decreeing $P(x,y) \wedge Q(z) = R(x,y,z)$ whenever $P(x,y) \wedge Q(z)$ and $R(x,y,z)$ take the value $\top$ on the exact same subset of V³. (So, in the end, our Boolean algebra consists of equivalence classes of formulas, which I’m calling ‘predicates’.)

Okay—full steam ahead! Having looked at a function that’s an injection but not a surjection, it’s time to look at a function that’s a surjection but not an injection.

The simplest example is the one you described. Category theorists would call it the unique function from 2 to 1, but let’s call it

$g \colon \{x,y\} \to \{x\}$ .

First let’s think a minute about

$B(g) \colon B(\{x,y\}) \to B(\{x\})$ .

This takes any predicate P(x,y) and maps it to P(x,x).

So, what would a right adjoint of B(g) be like? It would need to map any predicate G(x) to a predicate H(x,y) such that

$P(x,x) \le G(x)$ iff $P(x,y) \le H(x,y)$

for all predicates P(x,y).

What must H(x,y) be, to make this true? It must be cooked up from G(x) somehow.

MW: Before answering that, I want to elaborate on the “semantics to syntax” conversion you sketched. You can take it one step further: given a structure M for a language L, introduce names (i.e., constants) for all elements in the domain of M. Then all information about M can be translated into syntax. Logicians call this the “method of diagrams”; it became a powerful tool in the hands of Abraham Robinson and others.

For example, if a formula is universal (a string of universal quantifiers in front of a quantifier-free formula), then it’s downwards absolute: “as above, so below”. Using the method of diagrams, you can show the converse: any downwards absolute formula is equivalent to a universal one. (This is just an outline—for a precise statement, consult the textbooks.)

OK, surjections. For the right adjoint, assume that $P(x,x) \le G(x)$ . Then we must have $(P(x,y) \wedge x=y) \le G(x)$ . Next we make use of a fact about Boolean algebras: $(A\wedge B)\le C$ if and only if $A \le (B\rightarrow C)$ . This gives $P(x,y) \le (x = y \rightarrow G(x))$ . We can run the whole argument in reverse, too, so we get

$P(x,x) \leq G(x)$ iff $P(x,y) \leq (x=y\rightarrow G(x))$

This is our right adjoint!

Next let’s figure out the left adjoint. We want to find H such that

$G(x) \leq P(x,x)$ iff $H(x,y)\leq P(x,y)$

To get H, we just copy G “along the diagonal”. As a predicate:

H(x,y) ≡ G(x) ˄ x=y

This reminds me of the meaning of “qualified quantifiers”, like (∀x<y)φ(x) and (∃x<y)φ(x). For the existential case, we explicate this using a conjunction: ∃x[x<y ˄ φ(x)]. For the universal case, we use an implication: ∀x[x<y → φ(x)].

JB: Thanks for explaining the method of diagrams! When we really get rolling into original research, we should find some slick category-theoretic way to say what it does.

And now, let celebrate: Hurrah! We’ve gotten equality to emerge from thin air, by demanding that our Boolean algebra homomorphism B(g) has a right and left adjoint!

The right adjoint gives

$P(x,x) \leq G(x)$ iff $P(x,y) \leq [x=y\rightarrow G(x)]$ .

while the left adjoint gives

$G(x) \leq P(x,x)$ iff $[G(x) \wedge x=y] \leq P(x,y)$

So quantifiers and equality are not merely things our ancestors stuck into the predicate calculus because they were so very wise: these concepts arise automatically from some general principles!

The appearance of the implication or ‘material conditional’ $\rightarrow$ when we do the right adjoint and the conjunction $\wedge$ when we do the left adjoint can’t be an accident. Any element p of a Boolean algebra B gives an operation on B

$q \mapsto p \wedge q$ .

This is a functor from B to itself, and it has a right adjoint that does this:

$r \mapsto p \rightarrow r.$

This is easy to check: it just says that

$p \wedge q \le r$ iff $q \le p \rightarrow r.$

So, serious categorical logicians say implication is right adjoint to conjunction. We skipped over a whole mini-course where I’d motivate Boolean algebras—and the more general Heyting algebras, which are the generalization of Boolean algebras to intuitionistic logic—starting from category theory. I wanted to get straight to the predicate calculus, so I decided to take propositional calculus for granted! But the way implication shows up as a right adjoint is very nice.

I’m not quite sure how this connects to what you just said about “qualified quantifiers”, but it must be related. Indeed you used it in your argument.

MW: Hmm, and here’s another thing: the injection f we just looked at is a right inverse to g. I wonder if that shakes loose anything interesting.

JB: Wow! Nice idea! I think it does.

If f, g are monotone maps of posets that have right adjoints, say f* and g*, then the composite gf, if it exists, will also have a right adjoint (gf)*, given by

(gf)* = f* g* .

This is absurdly easy to see straight from the definition of adjoint I gave earlier—the definition in the case of posets.

So your observation definitely does shake something loose. In our example gf is the identity, so the right adjoint of gf must be the right adjoint of the identity, which—as you can easily check—is the identity! So, it must be that f* g* is the identity.

What does it mean, concretely, to say that the right adjoint of g, followed by the right adjoint of f, gets us back to where we started? It should be some law of logic involving equality and universal quantifiers!

MW: As it’s time to walk the dog, this will have to wait for the next post. Maybe I’ll try explaining it to him!

JB: I think cats are better at category theory: dogs are too dogmatic. But let me know how it goes.

Prev TOC Next

	John Baez on Nonstandard Models of Arithmet…
	Michael Weiss on Nonstandard Models of Arithmet…
	Ali Enayat on Nonstandard Models of Arithmet…
	Erica R on Non-standard Models of Arithme…
	Stirling’s For… on Stirling’s Formula: Ahlf…

First-Order Categorical Logic 3

Leave a Reply Cancel reply

Recent Posts

Recent Comments

Archives

Categories

Meta

First-Order Categorical Logic 3

Share this:

Like this:

Related

Leave a Reply Cancel reply

Recent Posts

Recent Comments

Archives

Categories

Meta