MW: John, it’s been eons since we last discussed First-Order Categorical Logic: not since September 2019! (I read a lot of Russian novels during the break.) But New Year’s seems like a good time to resume the tale.
JB: Yes indeed! It’s been a long time, and it’s mostly my fault. Let’s see if we can get back up to speed.
MW: We left off with the stirring exhortation:
On to Gödel’s completeness theorem!
I’m too rusty to plunge right into that. By way of rust removal, I’ll start recapping Our-Story-So-Far.
One thing I found a bit confusing at first: the two levels of categories. At the outer level, we have FinSet and BoolAlg, and functors FinSet→BoolAlg. (We called these functors scaffolds.)
Say T is a theory and we have a finite set of variables in the language of T (aka L(T)). Say {x,y,z}. We then formed the boolean algebra BTform({x,y,z}). This is the set of all formulas in L(T), modded out by the “provably equivalent” relation. And we saw how get a functor BTform:FinSet→BoolAlg from that. That is, given any function, say f:{x,y,z}→{x,y,w}, we cooked up a boolean algebra morphism from BTform({x,y,z}) to BTform({x,y,w}).
Minor nitpick. Shouldn’t we be using FinVar instead of FinSet?
JB: Wait—what? What’s FinVar? Whatever this category is, if it’s not equivalent to FinSet, this is no nitpick! And if it is equivalent to FinSet, there’s no point in talking about it: in category theory, we impose the rule that we never do constructions that break if we replace a category by some equivalent category. This gives category theory a lot of its flexibility.
MW: On the other hand, given any set V (the domain or universe), and any finite set of variables like {x,y,z}, we have the boolean algebra BVrel({x,y,z}) of all relations, “indexed” by the variables x, y, and z.
Here again I have a nitpick: we always talked about Vn (V3 for x,y,z). We never spelled out how the “indexing” would take place. Seems like you’d have to use OrderedFinSet instead of FinSet. Maybe the easiest thing would be to use FinSetℕ in both cases, the category of finite subsets of ℕ.
JB: “Indexing”? Ugh, that’s the kind of bureaucracy we category theorists avoid. If I said V3 instead of V{x,y,z}, that was just a convenient abbreviation. When our finite set of variables is S, we build our boolean algebra using VS, the set of all functions from S to V. In category theory, “3” in an exponent, like V3, is intended as an abbreviation for whatever 3-element set we actually mean.
By the way, the category of finite sets is equivalent to the category of finite subsets of ℕ, and in category theory we treat equivalent categories as “equally good”. The category of finite sets is more elegant, so we talk about that. If you think it’s too large, you can use the category of finite subsets of ℕ, or your favorite category that has just one set of each cardinality 0, 1, 2, …, and functions between these. They’re all equivalent.
MW: Okay, that’s good. I hadn’t thought enough about FinSet. I started wondering, what if we look at some odd set like {🎄,🦒,ℍ} (Christmas tree, giraffe, quaternions)? Then we need to consider formulas like “🦒+🎄=ℍ”?
JB: What’s wrong with that? If you chose a version of set theory with giraffes as urelements, you can’t blame me for using giraffes as variables! And kids don’t seem to mind using fruits as variables—there are lots of puzzles like this now:
though this one is harder than most.
MW: Kids these days :-) ! Fair point, though.
Light is beginning to dawn about V3. Old-fashioned guy I am, I always read that as the set of (ordered) triples. Just writing “VS” instead of “V3” was the clue I needed. This is a communication issue, or maybe cultural. Of course I’m used to “VS” as notation for the set of functions from S to V. But I’m used to “V3” as a related notation, not a special instance of it.
JB: “Ordered triple” is fine until I ask you what an ordered triple is—does your set theory have ‘ordered triples’ as a primitive, or do you define (x,y,z) in terms of ordered pairs (there are two obvious ways), and then how do you define ordered pairs (there are various ways), etc. It’s a can of worms, and opening it won’t help us do interesting math.
In category theory we say: what matters is not how things are made, but what we can do with them. Leave every can of worms nicely sealed, and focus on its sleek exterior: its universal properties. All that matters about V3 is that if we have an element of it, we can extract 3 elements of V, one for each element of the set we’re calling “3”—and conversely.
MW: As for FinSet—it’s the category of finite sets, but finite sets of what? The elements come from a pool, let’s call it U—so it’s really FinSet(U). My “FinVar” is just FinSet(U) when U is the set of variables of the language of our theory T.
“Index” is not a dirty word for me, but has a very flexible meaning. Any time we have a function f:I→V, I sometimes think of the elements of I as indices. If f:{🎄,🦒,ℍ}→V, then f(🦒) is element indexed by 🦒.
JB: Okay, fine.
MW: I guess we’ll find out if we get some mileage out of using FinSet(U) instead of sticking with FinSet(ℕ), or if it’s just part of the ethos of category theory.
JB: The ethos of category theory is not to give a damn about the difference between equivalent categories. Use FinSet(U) or FinSet(ℕ) or the set of all grammatical English sentences if you want—just please don’t tell me about it, or do anything where matters! It would be like me telling you what I think the elements of Monster group actually are. That’s a non-issue, because any two simple groups with that same whopping number of elements are isomorphic. When we go up one notch from set to categories, we go from treating isomorphic things as “the same”, to treating equivalent things as “the same”.
MW: Hey, I’m not knocking ethos. Every branch of mathematics—heck, every branch of knowledge—has its own characteristic way of looking at things. Absorbing that matters as much as learning the facts, figures, theorems and definitions.
Category theory is not my native language. I became a little bit fluent a few years back, but I’ve been away from it for too long.
Anyway, we obtained a functor BVrel:FinSet→BoolAlg from all that. A so-called set-based scaffold.
But now for the inner level. Every boolean algebra is itself a category if you put on the right glasses! In particular, so is each BTform({x,y,z}) and each BVrel({x,y,z}). And the boolean algebra morphisms we ginned up are functors. With this observation, we got to “send in the adjoints”.
JB: Right: when you’re doing set theory, there are sets all over the place, and sets of sets, and sets of sets of sets, and it’s all very unsettling if you’re not used to it. In category theory there are categories all over the place, and BoolAlg is a category of categories.
This lets us take advantage of Lawvere’s incredible observation that logic is all about adjoint functors. Well, “all about” is an exaggeration, but it came as such a shock that it calls for a bit of hyperbole!
It all goes back to Lawvere’s 1969 paper Adjointness in Foundations. We’ve got a functor B: FinSet → BoolAlg. Thus, for any finite set—call its elements ‘variables’—we get a boolean algebra of propositions with those free variables. And for any map between finite sets, say f: S → T, we get a map of boolean algebras B(f): B(S) → B(T). This expresses how given a proposition we can get a new one by swapping out its free variables using f. But now we demand that B(f) has left and right adjoints! This gives us universal and existential quantifiers, and equality!
MW: Right. We called a scaffold with that property adjointful. And an adjointful scaffold satisfying the Beck-Chevalley and Frobenius conditions is, as I recall, a hyperdoctrine.
We’re getting closer to the completeness theorem. I can taste it! (Or maybe that’s the apple tart from last night?) I’m psyched we’re not leaving our discussion of it incomplete.
However, first I think we do need to review the adjoints. I don’t mind going over it: this stuff is cool! (Dope? Copacetic? Groovy? What do kids say these days—bussin?)
Merry Christmas and Happy Hanukah!
Diagonal Argument 