**MW:** An addendum to the last post. I *do* have an employment opportunity for one of those pathological scaffolds: the one where *B*(0) is the 2-element boolean algebra, and all the *B*(*n*)’s with *n*>0 are trivial. It’s perfect for the semantics of a structure with an empty domain.

The empty structure has a vexed history in model theory. Traditionally, authors excluded it from the get-go, but more recently some have rescued it from the outer darkness. (Two data points: Hodges’ *A Shorter Model Theory* allows it, but Marker’s *Model Theory: An Introduction* forbids it.)

All *n*-ary predicates with *n*>0 are universally true, because they’re vacuously true. But ∃*x*(*x*=*x*) is false, while ∀*x*(*x*=*x*) is true. So *B*(0) contains both verum ⊤ and falsum ⊥.

The empty structure looks a little sketchy in this sense: the standard rules of logic require modification for it. (That’s why you were able to prove that its logic isn’t a hyperdoctrine.) On the other hand, its good friends the number 0 and the empty set will vouch for its good character. Hodges allows it because it makes some theorems nicer.

**JB:** This is very interesting. Near the end of our last conversation I claimed without proof that the Frobenius condition implies

∃*x*(⊤) = ⊤.

I now think this was *wrong*. Without this, I don’t think we can rule out the hyperdoctrine where *B*(0) is the 2-element boolean algebra but all the *B*(*n*)’s with *n*>0 are trivial. And that makes me happy, because I really *don’t* want to rule out the empty model of first-order theories—that is, what you’re calling the ’empty structure’.

So let me revise some of my statements from the last episode. I want to define an **inconsistent** hyperdoctine *B* to be one with ⊤ = ⊥ in *B*(0), or equivalently, one where *B*(0) is the trivial boolean algebra. This implies that all the *B*(*n*)’s with *n*>0 are trivial.

If any *B*(*n*)’s with *n*>0 is trivial, then they all are—our techniques from last time do show this—but this does *not* imply that *B*(0) is trivial. There is a hyperdoctrine where *B*(0) is the 2-element boolean algebra but all the *B*(*n*)’s with *n*>0 are trivial. And this one is consistent.

To really prove this we should dig deeper into the Frobenius condition—and for that matter, the Beck-Chevalley condition. If I try to explain these to you, that will force me to understand me better.

But I think we’re okay for now. So, this time it’s for real: on to Gödel’s completeness theorem!