JB: Last time we saw how to get some laws of logic from two facts:
• right adjoint functors between boolean algebras preserve products (‘and’),
and
• left adjoint functors between boolean algebras preserve coproducts (‘or’).
To be precise, the fact about right adjoints gives all the laws shown in red below, while the fact about left adjoints gives us all the laws shown in blue:
| ∀y(A(x,y)∧B(x,y)) = ∀yA(x,y) ∧ ∀yB(x,y) |
| ∃y(A(x,y)∧B(x,y)) ≤ ∃yA(x,y) ∧ ∃yB(x,y) |
| x=y→(A(x)∧B(x)) = x=y→A(x) ∧ x=y→B(x) |
| x=y∧(A(x)∧B(x)) = x=y∧A(x) ∧ x=y∧B(x) |
| ∀y(A(x,y)∨B(x,y)) ≥ ∀yA(x,y) ∨ ∀yB(x,y) |
| ∃y(A(x,y)∨B(x,y)) = ∃yA(x,y) ∨ ∃yB(x,y) |
| x=y→(A(x)∨B(x)) = x=y→A(x) ∨ x=y→B(x) |
| x=y∧(A(x)∨B(x)) = x=y∧A(x) ∨ x=y∧(B(x) |
But you’ll notice we’re not getting the four laws in black—two being equations and two being inequalities (that is, implications). So how do we get those?
For starters, while right adjoint functors preserve products, any functor ‘half-preserves’ products. What I mean is this: if F: C → D is a right adjoint functor between categories that have binary products, and c,c′ are any two objects in C, then
F(c × c′) ≅ F(c) × F(c′)
If F is just any old functor there’s no reason for this to be true. But we still automatically get a morphism going between F(c × c′) and F(c) × F(c′) in one direction. That is, while they may not be isomorphic, they’re at least still ‘morphic’.
Are you familiar with this? Or can you figure out why it’s true, and which way the morphism goes?
MW: This looks pretty straightforward. Let’s take the case of a functor F applied to c∧c′. Now, c∧c′≤c and c∧c′≤c′, so F(c∧c′)≤F(c) and F(c∧c′)≤F(c′). But the conjunction in a boolean algebra is the greatest lower bound for its operands: if z≤x and z≤y, then z≤x∧y. (Which makes perfect sense if you read ≤ as “implies”. Also, that’s basically the definition of a product in a category.) Therefore F(c∧c′)≤F(c)∧F(c′).
The argument for ∨ is dual: the disjunction is the least upper bound. So we’ve obtained the two inequalities.
We also get one half of the two equations. Let’s look at one of these inequalities:
x=y∧(A(x)∧B(x)) ≤ x=y∧A(x) ∧ x=y∧B(x)
So what’s going on with the ≥ half? Clearly we’re using a special property of ∧: c∧c=c. We’re also using associativity and commutativity, but these are general properties of binary products, yes?
The story for the remaining inequality, with x=y→(A(x)∨B(x)), is dual, once we rewrite p→q as ¬p∨q.
JB: Great! This is really nice.
I was trying to get you to talk in the language of categories, but you perhaps wisely translated my puzzle into the language of posets, which is a special case (or Boolean algebras, the even more special case we’re actually concerned with now). Here’s how I would have answered my puzzle:
For any functor F: C → D between categories that have binary products, and any two objects c,c′ ∈ C, there’s a god-given morphism
F(c × c′) → F(c) × F(c′)
since any such morphism is the same as a pair of morphisms
F(c × c′) → F(c), F(c × c′) → F(c′)
and we get such morphisms by applying F to the projections
c × c′ → c, c × c′ → c′.
And in the case of a poset this gives exactly what you said!
MW: Wait a sec! What do you mean, the god-given morphism “is the same” as a pair of morphisms? Do you mean the universal property of products? That guarantees that the pair factors through a unique morphism F(c × c′) → F(c) × F(c′). Is that what you’re getting at?
JB: Yes. We category theorists say “this is the same as that” when there’s a natural bijection between two kinds of things. So when we say “a morphism from A to B×C is the same as a morphism from A to B and a morphism from A to C”, we mean “there is a canonical bijection between morphisms from A to B×C and pairs consisting of a morphism from A to B and a morphism from A to C”. And now you explained why there’s such a bijection.
By the way, it’s a common beginner’s mistake to think F preserves binary products if we always have
F(c × c′) ≅ F(c) × F(c′)
But this isn’t good enough! We need the god-given morphism F(c × c′) → F(c) × F(c′) described above to be an isomorphism. But for posets this issue goes away, since there’s always at most one morphism between objects!
Anyway, the fact that any functor between boolean algebras has F(c∧c′)≤F(c)∧F(c′) and F(c∨c′)≥F(c)∨F(c′) gives the inequalities shown in green here:
| ∀y(A(x,y)∧B(x,y)) = ∀yA(x,y) ∧ ∀yB(x,y) |
| ∃y(A(x,y)∧B(x,y)) ≤ ∃yA(x,y) ∧ ∃yB(x,y) |
| x=y→(A(x)∧B(x)) = x=y→A(x) ∧ x=y→B(x) |
| x=y∧(A(x)∧B(x)) = x=y∧A(x) ∧ x=y∧B(x) |
| ∀y(A(x,y)∨B(x,y)) ≥ ∀yA(x,y) ∨ ∀yB(x,y) |
| ∃y(A(x,y)∨B(x,y)) = ∃yA(x,y) ∨ ∃yB(x,y) |
| x=y→(A(x)∨B(x)) = x=y→A(x) ∨ x=y→B(x) |
| x=y∧(A(x)∨B(x)) = x=y∧A(x) ∨ x=y∧(B(x) |
It also predicts inequalities for the two items shown in black, but as you noted, these are equations thanks to the laws of a boolean algebra! So everything in our tables has been accounted for, purely from the fact that we have a functor B: FinSet → BoolAlg where every boolean algebra homomorphism B(f) has both a right and left adjoint!
MW: There’s also a categorical proof of the equations c∧c=c and c∨c=c. After all, c is clearly the greatest lower bound of the pair c,c. (And the least upper bound too.) But the glb property is just the universal property of products, when stated for a poset. So c∧c=c follows.
Hmm, I almost asked myself why this doesn’t prove that c×c=c for any category with products. I’ll leave that as a minor puzzle for our readers.
JB: On the one hand all this is very elegant, and we can triumphantly rest on our laurels. On the other hand, it leaves us in the dark as to what’s missing from our approach so far, and why we need the Beck-Chevalley and Frobenius conditions to fill in what’s missing. For readers late to the party, we already sketched out the answer in Part 4. For example, this Frobenius law gives this:
∃y(P(x)˄Q(y)) = P(x) ˄ ∃y Q(y)
It’s clearly something we want, and it’s nowhere to be found in our tables above.
Heh. We started down this road because I wanted us to get a better understanding of Beck-Chevalley and Frobenius. But so far we’ve only seen how much we can do without them! At this point I’m willing to reconsider, and try to do what you really want: prove Gödel’s completeness theorem in this framework. If you want, we can try to do it ignoring Beck-Chevalley and Frobenius. This has some virtues.
If we fail, maybe we’ll see why we need those extra rules to succeed. But if we succeed, we’ll have proved a more general version of Gödel’s completeness theorem: not just for hyperdoctrines, but for what we’ve called ‘adjointful scaffolds’: functors B: FinSet → BoolAlg where every boolean algebra homomorphism B(f) has both a right and left adjoint. (A plain ‘scaffold’ is just a functor B: FinSet → BoolAlg.)
It would be like the old joke where you take apart a watch, and put it back together, and it works, but you have two pieces left over!
MW: Yeah, let’s shoot for completeness! I suspect we will need Frobenius or something like it. Existential quantifiers are, in a way, the crux of Henkin’s proof. It would be astonishing if we could bag our game without employing their special properties.
But there’s one other issue we might want to address first: the scaffold for the empty domain. I suggested in post 6 that this should have B(0) non-trivial, with all B(n) trivial for n>0. Toby Bartels has made some intriguing comments about the empty domain in the last post.
What do you think?
JB: I vaguely recall from our last go at Gödel’s completeness theorem that we’ll need to understand the empty domain to correctly state in our new language the classic result that any consistent theory has a model in the old-fashioned sense. That is, I’m afraid we’ll need to sharpen this statement to make it nontrivial. Does an inconsistent theory have a model with an empty domain? I forget the details.
So sure, let’s think about this.
Diagonal Argument 
Since I’ve been pushing for allowing the empty domain, I’ll answer this question:
>Does an inconsistent theory have a model with an empty domain?
No; or at any rate, that shouldn’t be the case, and if it comes out that way in your framework, then I’d say that something went wrong. The theories with empty models are those with no constant terms and no existentially quantified axioms (or axioms logically equivalent to existential statements, such as ¬ ∀x P(x) or P ∧ ∃x Q(x)).
For example, the theory of semigroups has an empty model; that is, there is an empty semigroup. But the theory of monoids does not have an empty model; depending on how you formulate it, it either has a constant term or an existential axiom. On the other hand, the theory of monoids without identity is inconsistent and has no models at all.