Category Archives: Categories

First-Order Categorical Logic 6

Prev TOC

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!

Prev TOC

Leave a comment

Filed under Categories, Conversations, Logic

First-Order Categorical Logic 5

Prev TOC Next

JB: Okay, let me try to sketch out a more categorical approach to Gödel’s completeness theorem for first-order theories. First, I’ll take it for granted that we can express this result as the model existence theorem: a theory in first-order logic has a model if it is consistent. From this we can easily get the usual formulation: if a sentence holds in all models of a theory, it is provable in that theory.

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic

First-Order Categorical Logic 4

Prev TOC  Next

MW: I made up a little chart to help me keep all these adjoints straight:

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic

First-Order Categorical Logic 3

Prev TOC Next

JB: Okay, let’s talk more about how to do first-order classical logic using some category theory. We’ve already got the scaffolding set up: we’re looking at functors

B \colon \textrm{FinSet} \to \textrm{BoolAlg}.

You can think of B(S) as a set of predicates whose free variables are chosen from the set S. The fact that B is a functor captures our ability to substitute variables, or in other words rename them.

But now we want to get existential and universal quantifiers into the game. And we do this using a great idea of Lawvere: quantifiers are adjoints to substitution.

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic

First-Order Categorical Logic 2

Prev TOC Next

MW: So let’s see. Last time we talked about the functor B from the category FinSet to the category BoolAlg of boolean algebras. Liberal infusions of coffee convinced you that B is covariant; I accidentally suggested it was contravariant. I think I’ve come round to your position, but I still have a couple of things I want to say on the matter. If it won’t be too confusing for our readers.

JB: Okay.  If we’re planning to talk more about the variance, it’s probably good to start out by getting the reader a bit confused.  I used to always be confused about it myself.  Then I finally felt I had it all straightened out.  Then you shocked me by arguing that it worked the opposite way.  Your argument was very sneaky.

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic

First-Order Categorical Logic 1

TOC Next

(A conversation between John Baez and Michael Weiss.)

JB: Okay, maybe it’s a good time for me to unleash some of my crazy thoughts about logic. They’ve been refined a lot recently, thanks to all the education I’ve been getting from you and folks on the n-Category Café. So, I can actually start with stuff that’s not crazy at all… although it may seem crazy if you’re not used to it.

I’ll start with some generalities about first-order classical logic. (I don’t want to get into higher-order logic or intuitionistic logic here!) The first idea is this. In the traditional approach, syntax and semantics start out living in different worlds. In categorical logic, we merge those worlds.

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic