First-Order Categorical Logic 12

Prev TOC Next

MW: Last time we looked at the categorical rendition of “C is a model of B”:

• Functors B:FinSet→BoolAlg and C:FinSet→BoolAlg
• A natural transformation F:B→C

where B and C are hyperdoctrines, and

• B is syntactic: the elements of each B(n) are equivalence classes of formulas (which we agreed to call predicates);
• C is semantic: the elements of each C(n) are relations on a domain V.

(We’ve been saying that C(n) is the set of all n-ary relations on V, but I see no need to assume that.)

I know you categoriticians like to keep things abstract, but I have to touch ground frequently or I get light-headed. So here’s an example. Say B is LO, the theory of linear orderings. And say C is (ℕ,<). B(2) contains predicates like [y<x] and [∃z(y<z<x)]. F₂:B(2)→C(2) maps the predicates to the corresponding relations. At least that’s what we want F to do. For example, F₂([y<x]) should be the less-than relation on ℕ, and F₂([∃z(y<z<x)]) should be the relation “y precedes x, but not immediately”.

I raised what I called the “key question”: does F play nice with quantifiers? For example, let’s existentially quantify [y<x], getting [∃y(y<x)]. Suppose F₂([y<x]) is the less-than relation. (I’ll have more to say about that later.) Can we conclude, just from that fact that F is a natural transformation, that F₁([∃y(y<x)]) is the subset ℕ∖{0}?

I think the answer must be yes! We learned back in post 3 that “existential quantification is the left adjoint of injection”. In this example, the ∃y is the left adjoint to the morphism induced by the map {x}→{x,y}. That holds both “syntactically and semantically” (in both B and C). So if “natural transformations preserve adjoints”, we should be home free!

Complications: the adjoints don’t belong to BoolAlg, but to the larger category Poset. And I’m assuming the preservation property, just because that’s how category theory usually works. I haven’t tried to prove it.

(What about the “conservation of proof-energy” I mentioned last time? It would shift the difficulty to constructing the natural transformation.)

(Actually, Poset isn’t quite the category we need to consider. The objects still remain boolean algebras, but we want to allow all order-preserving maps as morphisms. PBoolAlg? PoolAlg? Now that I made up that last name, I don’t know if I like it—it sounds like you forgot to add the chlorine to the water!)

JB: It’s not clear we need to formally introduce this category to state or prove what we’re trying to prove, though it’s certainly lurking in the background somewhere. I think what we should do is precisely state what we’re trying to prove.

You stated it in general like this: “natural transformations preserve adjoints”. That’s a good rough statement of the goal, but it doesn’t make literal sense. Because adjoints of boolean algebra homomorphisms are not themselves boolean algebra homomorphisms, a natural transformation between boolean algebra homomorphisms doesn’t do anything to these adjoints: at least not in a literal simple-minded way.

We’ve got functors B:FinSet→BoolAlg and C:FinSet→BoolAlg. And we’ve got a natural transformation F:B→C. What F does, by definition, is give us for each object of FinSet a morphism in BoolAlg making a bunch of squares in BoolAlg commute: the “naturality squares”. Every arrow in such a square is a morphism in BoolAlg. It doesn’t make literal sense to say F is preserving some kind of map between boolean algebras that’s not a morphism in BoolAlg.

And yet we’re hoping it does preserve them… in some way that’s not so literal. So we need to state precisely what we’re actually hoping. Often in category theory it’s not very hard to prove things once we can state them precisely and keep very clearly in mind exactly what we just said. The hard part is getting the clear mental picture of what’s going on. And I don’t think we’re there yet. At least I’m not.

So let’s state exactly what we want, as clearly as we can. I think we have to keep that commuting square firmly in mind, since that’s all we’ve got. Two arrows in the square, let’s say the top and bottom ones, have adjoints going back that are not boolean homomorphisms. Let’s say left adjoints to be specific. Now, what are we hoping about this square?

MW: Hmmm…trickier than I imagined. I thought that expanding BoolAlg to PoolAlg would lead out out of our quandary. Or at least help. BoolAlg, I learn from Wikipedia, is a wide subcategory of PoolAlg. Let’s look at the injection {x}→{x,y}. The left adjoint is [Q(x,y)]↦[∃yQ(x,y)].

I imagined that the left adjoint would somehow fall out of F, which is now a natural transformation between functors from FinSet to PoolAlg. But that means it would have to be F({x,y}→{x}). That seems wrong. The map {x,y}→{x} renames y to x. That’s a far cry from quantifying out y.

JB: We’ve got two hyperdoctrines, which are functors B:FinSet→BoolAlg and C:FinSet→BoolAlg, and a natural transformation F:B→C. We’re trying to state a property we want F to have, so we can see if it follows from our framework so far. This property somehow involves adjoints of morphisms in BoolAlg.

So let’s see what we’ve got. By definition of ‘natural transformation’ each morphism f: m → n in FinSet gives a commuting square in BoolAlg. Should we figure out how to draw it? I see it hovering before me in my mind’s eye.

MW: You mean like this?

JB: Yes, that’s it! B(f) and C(f) have adjoints by the definition of hyperdoctrine. They have both left and right adjoints. Let’s take their left adjoints.

So we get a new square where the two horizontal arrows are pointing the other way. The two vertical arrows are unchanged. All these arrows are poset morphisms, so they’re morphisms in PoolAlg.

MW: Like this:

 

I’ve named the “syntactic” adjoint (∃y); it takes [Q(x,y)] to [∃yQ(x,y)]. For the “semantic” adjoint, I’ve named it sup_y, since back in post 3 you noted that sup_yR(x,y)=⊤ when and only when R(x,y)=⊤ for some y.

Caveat: these names are appropriate only when f:m→n is an injection. We established, way back when, that these are the left adjoints for an injection.

JB: The question screaming at me is this:

Does this new square commute?

I’m not sure that’s the right way to formalize our desire that F behaves nicely, but it seems like an obvious guess. In category theory squares should commute. They don’t always commute, but you should always want them to commute. That may be naive, but it’s generally a good first instinct.

So I can’t help but wonder: does the commutativity of this new square really say the thing we’re trying to say, about models playing nicely with existential quantifiers? I want to look at what it amounts to in a simple example.

MW: I think it’s what we want. Let’s take my example at the top of this post: B is LO, the theory of linear orderings. C is (ℕ,<). Also, f:{x}→{x,y}. A typical element of B(2) is [y<x]. Let’s go down and and then across. F₂ takes us to the “less than” relation on ℕ. The left adjoint sup_y takes us to the unary relation “x≠0″. Now let’s go across and then down. The syntactic left adjoint takes us to [∃y(y<x)]. We want this to map to that relation “x≠0″. If it does, then the diagram commutes, and the existential quantifier has been respected. At least in this case.

(Reminds me of that episode of Curb Your Enthusiasm: “You don’t respect wood!“)

JB: I like that show, which I tend to watch in airplanes, but I hadn’t seen that episode.

Anyway: great!

We had two ways to attack this problem. One was to figure out what how we want F to behave and then formalize that using category theory. The other was to use the “tao of mathematics”: draw the situation we’re studying as a diagram and hope that the commuting of this diagram expresses how we want F to behave. At first I wanted to take the first approach, since it’s level-headed and rational, and I’m trying to set a good example. The second approach has no real right to work: it expresses faith in the “unreasonable effectiveness of mathematics”. But it has an amazing tendency to work, at least in category theory, and it seems to have done so again!

So while you considered just one example, and one where f is monic and we take the left adjoints of B(f) and C(f), my experience with the unreasonable effectiveness of category theory makes me optimistic that we always want this square to commute. We can check various cases to see if this commutativity says reasonable things in every case. It should talk about how our model F respects existential and universal quantifiers, equality, etc.

Assuming I’m right, the question is then whether such squares automatically commute, or whether we need to impose their commutativity as an extra condition in the definition of “model”.

For this, I urge that you take a gander at the nLab’s definition of the Beck-Chevalley condition. It involves a square of functors which commutes up to natural isomorphism, and the condition says that when we take the left adjoints of its top and bottom arrows, the resulting new square still commutes up to natural isomorphism! Luckily this condition simplifies in our situation here, because our categories are posets, and functors between posets are naturally isomorphic iff they are equal.

The Beck-Chevalley condition is not always true: that’s why it’s called a “condition”. But it might be automatically true in our context. Or maybe not.

We saw the Beck-Chevalley condition before, in the very definition of hyperdoctrine, back in Part 4. Now we seem to be seeing it in a new context, in the definition of “model”, or map between hyperdoctrines! But could this be related?

MW: Hmmm… This is going to take some thought.

Prev TOC Next