MW: So let’s see. Last time we talked about the functor B from the category FinSet to the category BoolAlg of boolean algebras. Liberal infusions of coffee convinced you that B is covariant; I accidentally suggested it was contravariant. I think I’ve come round to your position, but I still have a couple of things I want to say on the matter. If it won’t be too confusing for our readers.
JB: Okay. If we’re planning to talk more about the variance, it’s probably good to start out by getting the reader a bit confused. I used to always be confused about it myself. Then I finally felt I had it all straightened out. Then you shocked me by arguing that it worked the opposite way. Your argument was very sneaky.
MW: I didn’t mean to be sneaky, I just kind of stumbled into it! Here’s where I think I went astray. I said: an n-ary predicate is a function from Vn to {true, false}. A point in Vn is an n-tuple (x1,…,xn), which we can think of as a function from {1,…,n} to V, thus: 
with P being the n-ary predicate. But that composition isn’t right. If we start with i, we’d have
because P takes as input an n-tuple, not a single component xf(i).
We can still use the pullback trick to beget the m-tuple (xf(1),…,xf(m)) from the n-tuple (x1,…,xn). Hmm, P better take m-tuples as input, if we don’t want another ERROR! Ok, say P is an element of B(m), and f:{1,…,m}→{1,…,n}, and x is an n-tuple. Then 
Hmm… I was thinking about the case where f is a surjection. But it also works for injections. Say m=2 and n=3, and f is the function from {1,2} to {1,2,3} with f(1)=1 and f(2)=3. We start with a 2-ary predicate P, say x1 = x2. The first pullback “thins out” the 3-tuple (x1,x2,x3) to (x1,x3), and the second pullback gives us the “3-ary” predicate x1 = x3—which is 3-ary only in the sense that the emperor really was wearing new clothes.
In fact, the two pullbacks work just fine for any function f whatsoever.
We also have our other example of a Boolean algebra, namely equivalence classes of formulas. I’ve thought about this for a bit. But I think I’ve said enough for the moment.
JB: Okay. I agree with everything you just said. It’s good that we got those pullbacks straightened out, and I hope all our readers dwell on them for long enough to really understand, because getting this issue straight is a prerequisite for all the fancier stuff we’ll be doing.
By the way: don’t be disheartened! Category theory reduces all of mathematics to the study of arrows. The only mistake you can make with an arrow is get confused about which way it’s pointing. And so, in category theory we spend endless hours confused about which way the arrows are pointing.
I think we now have a choice before us. One choice, the high road, is to figure out how quantifiers get into the game. So far we have a humble functor
which assigns a Boolean algebra of predicates to any set of variables. These Boolean algebras let us do “and”, “or”, “not” and the like, and the functoriality lets us do substitution of variables. But we really want to get quantifiers—“for all” and “there exists”—into the game. We could do it by brute forces, just putting them in and demanding that they obey the laws we want, and we’d get something very much like the polyadic Boolean algebra invented by Halmos.
But this brute-force approach is rather ugly. It’s much more slick, and enlightening, to get quantifiers into the game using adjoint functors. That’s how Lawvere did it! He called the resulting gadgets “hyperdoctrines”—a fearsome term for something that deserves a more descriptive name, like “first-order theories”.
- Bill Lawvere, Adjointness in foundations, Dialectica 23 (1969), 281–296. (Reprinted in Theory and Applications of Categories, 16 (2006), 1–16.)
And it turns out these adjoints will give us “equality” for free: that is, predicates that say things like x = y. As you know better than I, there’s “first-order logic” and its slightly more refined brother, “first-order logic with equality”. The categorical approach very naturally gives first-order logic with equality. Lawvere pointed that out here:
- Bill Lawvere, Equality in hyperdoctrines and comprehension schema as an adjoint functor, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), pp. 1-14.
So, instead of getting Halmos’ polyadic Boolean algebras, we’ll actually get something closer to Tarski’s “cylindric algebras”, which include equality.
All this is delightful.
But there’s a slight catch! The trick with adjoints will automatically give us some of the laws of first-order logic with equality. But it won’t give us all those laws. For that we need to impose two more conditions: Frobenius reciprocity and the Beck–Chevalley condition.
The good news is that these extra conditions aren’t made up from thin air: they also show up in group representation theory and the theory of presheaves. I want to explain them, and it should be quite a nice story.
The bad news is that it’ll take a while, and I’m dying to apply this new approach to first-order logic. Just yesterday, while sitting bored in a conference, I tried translating Gödel’s completeness theorem into this language and it turned out to be shockingly cute! It even gives me hope of finding a somewhat new proof!
So the high road is to talk about how adjoints bring quantifiers into the game, and discuss Frobenius reciprocity and the Beck–Chevalley condition. But the low road is to just assume that there’s some way to get quantifiers into the game, by brute force or elegant theory, and talk about applications of this way of thinking.
Either way, we should eventually get around to doing both. What do you prefer?
MW: I’m opting for the high road, at least for a few more posts. Logicians live and breathe quantifiers! Also, I remember Frobenius reciprocity from group rep theory—that was neat! And I’ve been fond of presheaves ever since learning about Riemann surfaces. I’ll enjoy running into these old friends in a new city.
JB: Okay, the high road it is! Put on your boots and get ready for some exercise!
Diagonal Argument 