MW: I made up a little chart to help me keep all these adjoints straight:
In each of the four diagrams, the left adjoint is on the left and the right on the right (duh!) Rather than making P(x) silently pretend-depend on y, I use the ˄y=y trick. Δ stands for the diagonal functor, taking Q(x,y) to Q(x,x).
So in the top left diagram, the injection induces “P(x) goes to P(x)˄y=y”. The right adjoint of that is “Q(x,y) goes to ∀yQ(x,y)”. Likewise for the other three diagrams.
Composing the two left-hand diagrams on the left (i.e., ˄y=y followed by Δ) gives “P(x) goes to P(x)˄x=x”. Great! {x}→{x,y}→{x} is the identity, and sure enough P(x) is equivalent to P(x)˄x=x. Composing the right adjoints (same two diagrams) yields “P(x) goes to ∀y[x=y→P(x)]”. It’s not too hard to see that these are also equivalent.
If we look at the right hand diagrams, and compose left adjoints, we get “P(x) goes to ∃y[x=y˄P(x)]”. Again equivalent.
So that’s the solution to my injection-surjection puzzle!
One more thing. With the chart we can compute the units and counits of the adjunctions, almost for free. Thus:
- Top left diagram: unit is P(x) ≤ ∀y[P(x)˄y=y], counit is ∀yQ(x,y)˄y=y ≤ Q(x,y). The unit is an identity.
- Top right diagram: unit is Q(x,y) ≤ ∃yQ(x,y)˄y=y, counit is ∃y[P(x)˄y=y] ≤ P(x). The counit is an identity.
- Bottom left diagram: unit is Q(x,y) ≤ x=y→Q(x,x), counit is x=x→P(x) ≤ P(x). The counit is an identity.
- Bottom right diagram: unit is P(x) ≤ x=x˄P(x), counit is x=y˄Q(x,x) ≤ Q(x,y). The unit is an identity.
I must say, it seems a rather odd-lot collection. At least some are special cases of the substitution axioms for equality.
Oh yes, my dog was dogmatic only about sniffing all the clover along the route.
JB: And cats are catmatic about sniffing catnip.
Great solution! This is important: it means we can use properties of adjoints to derive some laws involving quantifiers and equality. The reason this matters is that normally we have to put in these laws “by hand”, with no justification other than that they seem right. It would be really cool if some category-theoretic machine could just crank out the laws of first-order logic. Of course you could still ask why we’re using this machine rather than some other machine. I’m not saying the machine eliminates the mystery of why we use some laws for logic rather than others. But it does shed new light on it.
Let’s look at the laws you got! Right adjoints give a law governing ∀ and equality:
P(x) = y[x=y→P(x)]
Left adjoints give a law governing ∃ and equality:
P(x) = ∃y[x=y˄P(x)]
Note I’m writing these laws as equations because that’s what your calculation actually gives: equations in the Boolean algebra B({x}). But from these equations we can derive “tautologies”, meaning elements of B({x}) that equal ⊤: the top element of this Boolean algebra, affectionately called “true”. Here they are:
P(x) ↔ ∀y[x=y→P(x)]
P(x) ↔ ∃y[x=y˄P(x)]
Here ↔ is the biconditional, a binary operation that makes sense in any Boolean algebra.
So you see, we are starting to play a game where we try to recover all the laws of classical first-order logic starting from this setup: a functor
such that each B(f) has both a left and a right adjoint.
Unfortunately, it turns out that not all the laws follow from just this! Fortunately, people seem to know exactly what’s missing, and how to fix it. Unfortunately I don’t understand this very well: I’m just learning it.
One thing that’s missing, is the Beck–Chevalley condition. Here’s an example of what this says.
Take a guy P(x,y). Apply B(h) where
sends x to itself and y to z. Then do an existential quantifier over x. You get ∃x P(x,z).
Alternatively, first do an existential quantifier over x and then apply B(k) where
Again, you get ∃x P(x,z). So, I’ve described two maps from B({x,y}) to B({z}) that should be equal. However, apparently the framework we’ve got does not yield this! Our notation makes the equality look inevitable, but it seems that’s not true. We need our functor B to obey the Beck–Chevalley condition, to get substitution and existential quantifiers to ‘commute’ with each other in a suitable sense.
Luckily, the Beck–Chevalley condition has a nice category-theoretic meaning: I’ve run into it in completely different contexts, like topological quantum field theory! But it’s still a bit mysterious to me.
Apparently we also need something else: the Frobenius condition. This gives us things like
∃y(P(x)˄Q(y)) = P(x) ˄ ∃y Q(y)
In other words, we can pull a conjunction out of an existential quantifer if the predicate involved, here P(x), doesn’t involve the variable we’re quantifying over.
So, my question now is: do you want to dig into these issues, or should we just assume someone has worked them all out?
MW: Yikes! The Beck-Chevalley and Frobenius conditions look like heavy-duty categoriosity. I think I’m ready to move on to applications.
JB: When you say that the Beck–Chevalley and Frobenius conditions are “heavy-duty”, you just make me want to explain them. They’re not that bad!
For example, the really good way to state the Frobenius condition is to say that for any function f between finite sets, B(f) preserves implication. With a little fiddling around, we can use this fact to derive rules like this:
∃y(P(x)˄Q(y)) = P(x) ˄ ∃yQ(y)
So none of this is extremely stressful. But like you, I’m eager to move on to applications.
MW: But first I want to make sure I follow what’s going on. Our two favorite functors B: FinSet → BoolAlg, Bform and Brel, satisfy the Beck–Chevalley condition and Frobenius reciprocity, right?
JB: Right. I tried to persuade you that these extra conditions are familiar laws of logic, which hold in every example of type Bform. I also pointed out that every example of type Brel is isomorphic to one of type Bform: you just cook up a theory in first-order logic with an n-ary predicate P for each n-ary relation on your chosen set V.
MW: But an arbitrary functor from FinSet to BoolAlg might not obey these extra conditions?
JB: I guess not.
MW: Oh yeah, not an arbitrary functor, but one satisfying all this adjoint stuff we’ve been discussing. Let’s call it an adjointful functor.
JB: Right. It must be possible for an adjointful functor B: FinSet → BoolAlg to fail to obey Beck–Chevalley and Frobenius, or obey just one of these conditions yet not the other. Otherwise, why would they impose both these extra conditions? These category-theoretic logicians aren’t stupid! But I haven’t seen counterexamples yet. I’ll have to find some.
MW: Also, people are convinced that adjointfulness and Beck–Chevalley and Frobenius are all we need to demand of B. Why? Some sort of representation theorem? Maybe, any such functor is naturally isomorphic to an instance of Bform?
JB: Actually this should be straightforward. Just take the usual laws of first-order logic with equality, and show they hold for any adjointful functor B: FinSet → BoolAlg obeying Beck–Chevalley and Frobenius. That means these laws are enough. To show they’re not too much, take the entire definition of “adjointful functor B: FinSet → BoolAlg obeying Beck–Chevalley and Frobenius” and see what it says for our example Bform. We did a few pieces of that exercise. But if we did it thoroughly, we could show that all we get are familiar laws of first-order logic with equality.
None of this can possibly require any cleverness. Persistence must suffice. The upshot will be a representation theorem of the sort you describe: every functor B obeying all these conditions is naturally isomorphic to a functor Bform: that is, one coming from a theory in first-order logic with equality.
Someone should have done this, but I don’t know where.
By the way, we don’t need to require both left and right adjoints. If you have left adjoints, you get right adjoints for free, and vice versa! The reason is that we’re working with Boolean algebras, which are isomorphic to their opposites. In more logician-friendly lingo, what I’m saying is that
∀ = ¬∃¬
This is true in classical logic; in intuitionistic logic, which category theorists often favor, it’s not. They use Heyting algebras instead of Boolean algebras.
It’ll be trickier to show that Beck–Chevalley and Frobenius are both actually needed: that you can’t derive either from the other in the presence of adjointfulness. To do this, I might look for some counterexamples. I’ll work away at this in my spare time, or break down and ask people on the n-Category Café.
But for now, let’s move on to some applications.
MW: Onward to Gödel completeness!
Diagonal Argument 