MW: Last time we reviewed the four adjoints:
| Q(x,y) ↦ ∀yQ(x,y) | right adjoint to B(f) for f:{x}→{x,y} |
| Q(x,y) ↦ ∃yQ(x,y) | left adjoint to B(f) for f:{x}→{x,y} |
| P(x) ↦ x=y→P(x) | right adjoint to B(g) for g:{x,y}→{x} |
| P(x) ↦ x=y∧P(x) | left adjoint to B(g) for g:{x,y}→{x} |
B(f) and B(g) are boolean algebra homomorphisms, preserving ¬, ∧, ∨, and ⊤and ⊥. But their adjoints might not be. Let’s check it out! We want to check the equations φ(¬A(x)) = ¬φ(¬A), φ(A∧B) = φ(A)∧φ(B), etc. for each of the adjoints. Pretty straightforward. Here are the resulting equations and inequalities.
φ(¬A) ?=? ¬φ(A)
| ∀y(¬A(x,y)) ≤ ¬∀yA(x,y) |
| ∃y(¬A(x,y)) ≥ ¬∃yA(x,y) |
| x=y→(¬A(x)) ≥ ¬(x=y→A(x)) |
| x=y∧(¬A(x)) ≤ ¬(x=y∧A(x)) |
Quantification gives us only one-way implications, not equality. And those implications come with a caveat: we’re assuming a non-empty domain. For then ∀y(something(y)) implies ∃y(something(y)), because there’s at least one element in the universe. But if you allow an empty domain, then you don’t get even those implications. (We discussed the empty domain in post 6.) Propositionally, ¬(p→q) implies p→¬q. That’s because ¬(p→q) means p is true and q is false, and p→¬q holds in that case. This accounts for the third line of the table.
φ(A∧B) ?=? φ(A) ∧ φ(B)
| ∀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) |
This time we have equations except for ∃, the second line of the table. Here, the left hand side says (for a given x) that the A and B sets have a non-empty intersection; the right hand side, that these two sets are each non-empty. So the left hand side implies the right hand side but not conversely.
φ(A∨B) ?=? φ(A) ∨ φ(B)
| ∀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) |
With ∨, the stories for the first two lines are switched. If the A or B set is everything, then their union is everything, but not conversely. The easiest way to see that the third line is correct: the only way p→(q∨r) can be false, is to have p true, and q and r false. That’s also the only way (p→q)∨(p→r) can be false.
φ(⊤) ?=? ⊤, φ(⊥) ?=? ⊥
| ∀y(⊤) = ⊤ | ∀y(⊥) = ⊥ |
| ∃y(⊤) = ⊤ | ∃y(⊥) = ⊥ |
| x=y→⊤ = ⊤ | x=y→⊥ ≥ ⊥ |
| x=y∧⊤ ≤ ⊤ | x=y∧⊥ = ⊥ |
The empty domain issue rears its head with just one equation: ∃y(⊤)=⊤. With an empty domain, this changes to ∃y(⊤)=⊥, since there doesn’t exist anything. Otherwise, nothing much to see here.
JB: Very nice! I want to see how we get all the facts in these tables from the definition of hyperdoctrine.
MW: Sounds good. By the way, in a comment to the last post, Toby Bartels gave neat general formulas for the adjoints. I’ll repeat them, expressed a little differently. Let f:{x1,…,xn}→{y1,…,ym}, and suppose f(xi)=yσi. Also assume that none of the y’s appears among the x’s. Then the right adjoint for B(f) is
P(y1,…,ym) ↦ ∀y1…∀ym(yσ1=x1 ∧ … ∧ yσn=xn → P(y1,…,ym))
and the left adjoint is
P(y1,…,ym) ↦ ∃y1…∃ym(yσ1=x1 ∧ … ∧ yσn=xn ∧ P(y1,…,ym)).
Since the y’s are dummy variables, if there is overlap between the x’s and y’s, just rename the y’s. Toby also points out that if one the y’s is the same variable as the corresponding x—that is, yσi. is syntactically identical to xi—then instead of renaming it, we can just omit the identity xi=xi and the quantifier ∀xi or ∃xi. This results in the formulas we had in the last post, for our two examples.
JB: Okay. Back to your tables. They nicely show what the left and right adjoint maps between boolean algebras preserve, in the examples we’re looking at. But we might also want to see how much they automatically preserve, just by the fact that these maps are left and right adjoints, and what other rules we’ll need to stick in by hand. Those should be the Beck–Chevalley and Frobenius rules.
We don’t need to do this, but it’s easy and fun. Let me show you an example of what I mean. Any functor that is a right adjoint preserves products and terminal objects. These facts are extremely easy to prove from the definitions—should we do it, or just take them for granted?
MW: Take them for granted. Plenty of good intros to category theory out there. Tom Leinster’s Basic Category Theory (my favorite) has these facts as special cases of Theorem 6.3.1. (I wrote up solutions to almost all of Leinster’s exercises.)
JB: Okay, good. Here’s why these facts about right adjoints matter now: in a boolean algebra, viewed as a category, the product of two objects is their ∧. In other words, having a morphism from p to q together with a morphism from p to r is the same as having a morphism from p to q ∧ r. In still other words,
Thus, any of the maps between boolean algebras that we got from right adjoints must preserve ∧. This principle instantly gives us two of the laws you wrote down:
and
Similarly, in a boolean algebra, viewed as a category, true is terminal. In other words,
“Everything implies the truth”. Thus, the maps between boolean algebras that we got from right adjoints must also preserve ⊤. This gives two more laws:
and
So we get four laws of logic just from the fact that right adjoints preserve products and terminal objects. Dually, left adjoints preserve coproducts and initial objects. And in a boolean algebra, the coproduct of two objects is their ∨, while the initial object is false or ⊥. So we get four more laws from this!
MW: Neat! And this demonstrates the laws for any map of FinSet, not just for injections and surjections. Although any such map is composed of a surjection and an injection, so that’s another way to see it.
Are we doing Beck-Chevalley and Frobenius next time?
JB: We probably should. To prove a version of Gödel’s completeness theorem I want to construct a Henkin-like model of any consistent theory. I think checking that this really works may force us to know exactly what are all the rules of a hyperdoctine.
Another approach would be to put this off until we know we care about it. But having assembled your tables of what happens with left and right adjoints, it’s probably good to figure out now how we can get everything in those tables from the rules of a hyperdoctrine. I pointed out that we could get eight rules just from the properties of adjoints. But in fact we can get a bit more! However, we must not be able to get all the usual rules of logic—that’s why we need Beck-Chevalley and Frobenius.
So, I think it’s best to straighten this stuff out now.
Diagonal Argument 
As a category theorist, I don’t like assuming an inhabited (= non-empty) domain. That’s bound to cause trouble down the line, just like assuming that every ring is non-trivial, every vector space has positive dimension, or just generally that every set is inhabited.
And you don’t have to! You have at least one free variable in all of these statements, so you can use that. (Even in the first half is the table for ⊤ and ⊥, the free variable is still there in the context even though it doesn’t appear in the statement.) For example, to prove that ∀y(¬A(x,y)) entails ¬∀yA(x,y) using only reasoning valid in first-order classical logic regardless of domain, you instantiate y in ∀y(¬A(x,y)) with x to get ¬A(x,x), then (by way of contradiction) do the same in ∀yA(x,y) to get A(x,x), achieving the desired contradiction. No need to pass through ∃y(¬A(x,y)) (although because x is around, you could prove that too).
That said, if you want a really pure example of quantification from adjoints, then instead of looking at the adjoints to B(f) for f:{x}→{x,y}, you should look at the adjoints to B(f) for f:∅→{y}. Then there is no free variable, and you get fewer implications. (Besides the two you noticed, ∀y(⊥) = ⊥ weakens to ∀y(⊥) ≥ ⊥.)
By the way, there’s a typo in the last line of the table for ¬; you wrote = here, but (as the following text acknowledges) it should be ≤.
The empty domain issue is vexed, and has been for a long time. You’d kinda like all the formulas ∀xφ(x) to be true, all the formulas ∃xφ(x) to be false, and all the usual rules of logic to hold. In particular, ∃xφ(x) should be equivalent to ¬∀x¬φ(x). Indeed, some authors treat ∃ as just an abbreviation for ¬∀¬ (or vice versa).
Problem is, as you’ve shown, that you can derive ∃xφ(x) from ∀xφ(x) using the usual rules. Mendelson (Introduction to Mathematical Logic, 5th ed., §2.16) is one author who has given a reasonably extensive discussion. He considers only sentences (closed formulas). He lets all sentences ∀xφ(x) be true. Any other sentence is a propositional combination, which he evaluates with the usual truth tables, after having replaced all the ∀xφ(x)’s with ⊤. Finally, he treats ∃xφ(x) as an abbreviation for ¬∀x¬φ(x).
He distinguishes between logically valid sentences (true in all non-empty domains) and inclusively valid ones (true in all domains). He gives this example: Let θ be a sentence. Then
∀x(θ∧¬θ)→(θ∧¬θ)
is logically valid but not inclusively valid, since we get ⊤→⊥ in the empty domain. Mendelson gives inference rules and axioms for inclusive validity.
I think this is why most logicians prefer to steer clear of the whole mess. It may be that in categorical logic, ignoring the empty domain will come bite us in the ass. In traditional logic, as Mendelson says, “an interpretation with an empty domain has little or no importance in applications of logic.”
I’m not convinced that the “right” approach to logic with an empty domain has been unearthed. Maybe it’s like the field with 1 element!
Thanks for pointing out the typo. Also, I agree about looking at f:∅→{y}.
It depends what you mean by ‘the usual rules’, but I would argue that you can only derive ∃xφ(x) from ∀xφ(x) in a context with a term (such as a free variable or a constant supplied by the language). Categorial logic plays a lot more attention to context than traditional logic; for example, we care about free variables even when they don’t actually appear in an expression. We also want to consider the category of all contexts, so even if one usually applies logic to inhabited contexts, the empty context may still be there in the category (as the initial object).
In the not so distant past, 1 was widely considered to be a prime number, the zero ring was widely considered not to be a ring with identity, and ‘all X are Y, therefore some X are Y’ was widely considered to be a valid syllogism; although we now acknowledge that all these are, if not exactly incorrect (because a matter of definition), at least inelegant. A vestige of this last one still remains in the minds of traditionalist logicians, but there’s no question in my mind what the elegant solution is: to allow the empty domain. (See https://ncatlab.org/nlab/show/too+simple+to+be+simple for more examples of this phenomenon.)
Yes, there are more theorems of logic if you restrict to inhabited domains (essentially adopting ∃y(⊤) as an axiom). On the other hand, there are more theorems if you restrict to subsingleton domains (where all terms are equal, essentially adopting ∀x∀y(x=y) as an axiom). These have a beautiful symmetry when it comes to the quantifiers! When considering f:∅→{y}, we find that ∀y(¬A(y)) ≤ ¬∀yA(y), ∃y(¬A(y)) ≥ ¬∃yA(y), ∃y(⊤) ≥ ⊤, and ∀y(⊥) ≤ ⊥ hold if (but only if) we restrict to inhabited domains. Conversely, ∀y(¬A(y)) ≥ ¬∀yA(y), ∃y(¬A(y)) ≤ ¬∃yA(y), ∃y(A(y)∧B(y)) ≥ ∃yA(y)∧∃yB(y), and ∀y(A(y)∨B(y)) ≤ ∀yA(y)∨∀yB(y) hold if (but only if) we restrict to subsingleton domains. (Also in subsingleton domains, all of the implications involving equality work both ways, which is no surprise since equality is trivial in that case.) Every other implication holds no matter what; therefore, every implication holds if the domain is both inhabited and a subsingleton, in other words if it’s a singleton. And that’s no surprise, since quantification is (also) trivial in that case.
The final argument is that we can figure out what ∀y(⊥) means using the universal property of the adjoint. If we’re looking at f:{x}→{x,y}, then A(x) ≤ ∀y(⊥) holds in B({x}) iff B(f)A(x) ≤ ⊥ holds in B({x,y}), and if we apply B(g) to this (where g:{x,y}→{x}), we get A(x) = B(g)B(f)A(x) ≤ B(g)⊥ = ⊥. (Here it’s essential that f has a one-sided inverse g.) So A(x) ≤ ∀y(⊥) holds only when A(x) = ⊥, and therefore ∀y(⊥) = ⊥. However, if we’re looking at f:∅→{y}, then there is no one-sided inverse, and this argument fails; we can still say that A ≤ ∀y(⊥) holds in B(∅) iff B(f)A ≤ ⊥ holds in B({x}), but that’s all. And if B is the pathological (but consistent) hyperdoctrine where almost every boolean algebra is trivial but B(∅) is not, then even B(f)⊤ = ⊥ in B({x}) and so ⊤ ≤ ∀y(⊥) and thus ∀y(⊥) = ⊤ in B(∅) (so ∀y(⊥) = ⊥ fails).