MW: Last time we justified some equations and inequalities for our adjoints: they preserve some boolean operations, and “half-preserve” some others. And we incidentally made good use of the color palette!
(Side note: I seem to recall that someone once did an edition of Euclid in color, making it easier to follow the proofs. Ah yes, here it is: The First Six Books of The Elements of Euclid in which Coloured Diagrams and Symbols are Used Instead of Letters for the Greater Ease of Learners, by Oliver Byrne. Love those 19th century titles.)
Anyway, the completeness theorem says that every consistent theory has a model. In post 6 we decided that ‘consistent’ means B(0) is the two-element boolean algebra {⊤,⊥}; for an inconsistent scaffold (functor from FinSet to BoolAlg), B(0) has just one element ⊤=⊥.
For the empty structure, B(0) still has two elements, but all the B(n)’s with n>0 are trivial.
Toby Bartels had some interesting things to say about the empty structure in comments to post 9. Should we look at those?
JB: Maybe let’s try to start proving the completeness theorem: we’ve been threatening to do so many years! Our readers may give up on us if we don’t do it now. We can think about the empty structure as needed while trying to prove this result. I have a feeling it’s going to come up.
When proving a theorem, it’s generally regarded as helpful to state it first. In real life, one often knows how to state it correctly only after having tried and failed to prove some wrong versions. But it’s still good to try.
So let’s see if we can state completeness for hyperdoctrines. We tried doing this in post 5, almost five years ago. I’ll cheat and read what I wrote.
I wrote: completeness states that if a hyperdoctrine
B:FinSet→BoolAlg
is consistent it has a model. We said B is consistent if B(0) is the two-element boolean algebra {⊤,⊥}. And we said a model of a hyperdoctrine B is a natural transformation from B to a hyperdoctrine
C:FinSet→BoolAlg
that has this special property: there is some set V called the universe for which
C(n) = P(Vn)
Here P means ‘power set’.
After thinking about it a little… like, umm, five years… I believe this statement is not quite what we want! I claim that with the current definitions, any hyperdoctrine, consistent or not, has a model. Do you see why I think that? (I gave a hint.)
MW: By “hint”, perhaps you meant this remark you made at the end of the last post:
Does an inconsistent theory have a model with an empty domain? I forget the details.
Let’s see what P(Vn) looks like when V=∅. ∅n=∅ for n>0 and P(∅)={∅}. So each B(n), n>0, is the trivial boolean algebra, with ⊥=⊤. This makes sense: the only n-ary relation on the empty set is the empty relation.
What about ∅0? That’s a one-element set, containing just the empty function (also denoted ∅, because it is the empty set). So P(∅0)=P({∅})={∅, {∅}}={⊥,⊤}.
For an inconsistent theory T, all its boolean algebras are trivial: any two n-ary formulas are provably equivalent. Even when n=0!
JB: So you’re saying I was wrong: not every hyperdoctrine has a model, because an ‘inconsistent hyperdoctrine’ doesn’t have a model.
Let me spell it out pedantically here.
By inconsistent hyperdoctrine I mean any hyperdoctrine
B:FinSet→BoolAlg
that assigns every finite set the terminal boolean algebra. There are lots of terminal boolean algebras but they’re all isomorphic so we call them all “the” terminal boolean algebra. Similarly, all inconsistent hyperdoctrines are isomorphic so we can talk about “the” inconsistent hyperdoctrine if we like.
It’s easy to see that a boolean algebra is terminal iff it has just one element. So, in a terminal boolean algebra the top element is the bottom. It’s an Orwellian situation: “up is down, true is false, ⊤ = ⊥”. There is no boolean algebra homomorphism from the terminal boolean algebra to any other boolean algebra, because it would have to map ⊤ = ⊥ to both ⊤ and ⊥ in the other boolean algebra, where they are distinct elements.
You seem to be telling me that an inconsistent hyperdoctrine B doesn’t have a model: that is, it doesn’t have a natural transformation to any hyperdoctrine
C:FinSet→BoolAlg
for which
C(n) = P(Vn)
for some set V. A natural transformation F from B to C would give a boolean algebra homomorphism
F0: B(0) → C(0)
But this does not exist, since B(0) is the terminal boolean algebra, while C(0) is never terminal, because it’s P(V0), which is the power set of a one-element set.
All this looks right to me. Okay, so it’s looking like we want to prove this:
A hyperdoctrine has a model iff it is consistent.
The important part is the “if”, but we’ve just seen the “only if”, so we might as well throw that in.
Now, I have a bunch of ideas for how to prove this, though they don’t add up to an actual proof yet. Should I start talking about those? Or maybe you have questions about what I just said… or maybe I screwed up again!
MW: There’s an issue. In post 5, we talked about the morphisms of BoolAlg. There are order-theoretic morphisms, and the more restricted class of algebraic morphisms. Only the latter have to preserve the boolean operations, including negation. The former need preserve only the order.
We agreed that we want BoolAlg to include all the order-theoretic morphisms—some of those adjoints don’t preserve negation.
The definition of “natural transformation” gives us a morphism F0, but how do you know it’s algebraic?
I’m pretty sure you can’t prove this, because there is a natural transformation from the inconsistent theory B to the empty structure C. In fact, two of ’em! All the B(n) and C(n) are the trivial boolean algebra, except for C(0). So all the morphisms Fn:B(n)→C(n) with n>0 are identities. There are two choices for F0: ⊤=⊥ goes to either ⊤ or ⊥. They both work. All the squares commute. Check it out!
We clearly want all the Fn’s to be algebraic morphisms, so I think we just put this in by hand, as part of the definition of a model.
As for whether we should include the empty structure, I’m agnostic. Whatever makes the theory smoothest. Let’s table that discussion till another time.
JB: You say “We agreed that we want BoolAlg to include all the order-theoretic morphisms….” But no, I never agreed with that! BoolAlg means the category of boolean algebras, and that means the morphisms are boolean algebra homomorphisms. These preserve all the structure of a boolean algebra, including negation, the chosen top element ⊤, and the chosen bottom element ⊥, and the operations ∧ and ∨.
I think you’re getting mixed up with how, in the definition of a hyperdoctrine, say our friend
B:FinSet→BoolAlg,
we demand that for each morphism f in FinSet, the boolean algebra homomorphism B(f) have a left and right adjoint. Those adjoints are typically not boolean algebra homomorphisms. They’re hardly ever so. But that’s okay: we never said they were morphisms in BoolAlg.
When we have a natural transformation F between functors B,C:FinSet→BoolAlg, as we’re now discussing, it sends each object n of FinSet to a morphism F: B(n) → C(n) in BoolAlg. And that’s a boolean algebra homomorphism. So we don’t have to stick this in by hand in the definition of model.
MW: Ah, OK. (Checks definitions.) But I think if you’ll reread the discussion in post 5, you’ll see why I thought we had settled on a “fuller” BoolAlg. On the other hand, if I’d reread the beginning of post 8, it would have cleared up my confusion.
Now for the key question: what about quantifiers? If [∃xφ(x)]=⊤ in B(0), then when the dust settles, we must have F0([∃xφ(x)])=⊤ in C(0). And this means that for some c∈V, [φ(c)] must equal ⊤ in C(0), in some sense. Does the “adjointful” condition give this to us with a magical puff of smoke?
My instincts say no. Boiled down to essentials, the Henkin proof of the completeness theorem (aka model existence theorem) rests on two constructions. The first, the “witnessing” step, insures that quantifiers are treated with respect. The second expands a possibly incomplete theory to a complete one, in order to define a “notion of truth”. (I gave a fuller summary in my post on the Arithmetized Completeness Theorem.)
I suspect that the “conversation of proof-energy” demands something equally elaborate in our situation.
JB: I see what tripped you up: in Part 5 I said “It’s probably good to recall why we need morphisms [between boolean algebras] that are just order-preserving, at least at certain points in our definition.” I was explaining that adjoints of boolean algebra homomorphisms are not themselves boolean algebra homomorphisms: they are more general morphisms, namely order-preserving maps. But they’re not morphisms in BoolAlg. They are morphisms in some other category.
If we redefined BoolAlg to have arbitrary order-preserving maps as morphisms, it would weaken the concept of hyperdoctrine to the point of near-uselessness. After all, we need renaming of variables to get along with all the boolean algbra operations. That’s what a functor
B:FinSet→BoolAlg
gives us.
We should investigate your “key question”. You seem to be asking whether in our approach to logic using hyperdoctrines, a model of a theory that says [∃xφ(x)]=⊤ must really have an element of the universe for which φ holds. Or something like that. I’m not even sure what I actually mean here. So yes, I suppose studying anything like the completeness theorem should wait until we answer this question of yours.
MW: Sounds good!
Diagonal Argument 