Category Archives: Logic

First-Order Categorical Logic 4

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

In each of the four diagrams, the left adjoint is on the left and the right on the right (duh!) Rather than making P(x) silently pretend-depend on y, I use the ˄y=y trick. Δ stands for the diagonal functor, taking Q(x,y) to Q(x,x).

So in the top left diagram, the injection induces “P(x) goes to P(xy=y”. The right adjoint of that is “Q(x,y) goes to ∀yQ(x,y)”. Likewise for the other three diagrams.

Composing the two left-hand diagrams on the left (i.e., ˄y=followed by Δ) gives “P(x) goes to P(xx=x”. Great! {x}→{x,y}→{x} is the identity, and sure enough P(x) is equivalent to P(xx=x. Composing the right adjoints (same two diagrams) yields “P(x) goes to ∀y[x=yP(x)]”. It’s not too hard to see that these are also equivalent.

If we look at the right hand diagrams, and compose left adjoints, we get “P(x) goes to ∃y[x=y˄P(x)]”. Again equivalent.

So that’s the solution to my injection-surjection puzzle!

One more thing. With the chart we can compute the units and counits of the adjunctions, almost for free. Thus:

  • Top left diagram: unit is P(x) ≤ ∀y[P(xy=y], counit is ∀yQ(x,yy=y ≤ Q(x,y). The unit is an identity.
  • Top right diagram: unit is Q(x,y) ≤ ∃yQ(x,yy=y, counit is ∃y[P(xy=y≤ P(x). The counit is an identity.
  • Bottom left diagram: unit is Q(x,y) ≤ x=yQ(x,x), counit is x=xP(xP(x). The counit is an identity.
  • Bottom right diagram: unit is P(x) ≤ x=x˄P(x), counit is x=y˄Q(x,x≤ Q(x,y). The unit is an identity.

I must say, it seems a rather odd-lot collection. At least some are special cases of the substitution axioms for equality.

Oh yes, my dog was dogmatic only about sniffing all the clover along the route.

JB: And cats are catmatic about sniffing catnip.

Great solution! This is important: it means we can use properties of adjoints to derive some laws involving quantifiers and equality. The reason this matters is that normally we have to put in these laws “by hand”, with no justification other than that they seem right. It would be really cool if some category-theoretic machine could just crank out the laws of first-order logic. Of course you could still ask why we’re using this machine rather than some other machine. I’m not saying the machine eliminates the mystery of why we use some laws for logic rather than others. But it does shed new light on it.

Let’s look at the laws you got! Right adjoints give a law governing ∀ and equality:

P(x)   =   ∀y[x=yP(x)]

Left adjoints give a law governing ∃ and equality:

P(x)  =   ∃y[x=y˄P(x)]

Note I’m writing these laws as equations because that’s what your calculation actually gives: equations in the Boolean algebra B({x}). But from these equations we can derive “tautologies”, meaning elements of B({x}) that equal ⊤: the top element of this Boolean algebra, affectionately called “true”. Here they are:

P(x) ↔ ∀y[x=yP(x)]

P(x) ↔ ∃y[x=y˄P(x)]

Here ↔ is the biconditional, a binary operation that makes sense in any Boolean algebra.

So you see, we are starting to play a game where we try to recover all the laws of classical first-order logic starting from this setup: a functor

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

such that each B(f) has both a left and a right adjoint.

Unfortunately, it turns out that not all the laws follow from just this! Fortunately, people seem to know exactly what’s missing, and how to fix it. Unfortunately I don’t understand this very well: I’m just learning it.

One thing that’s missing, is the Beck–Chevalley condition. Here’s an example of what this says.

Take a guy P(x,y). Apply B(h) where

h \colon \{x,y\} \to \{x,z\}

sends x to itself and y to z. Then do an existential quantifier over x. You get ∃xP(x,z).

Alternatively, first do an existential quantifier over x and then apply B(k) where

k \colon \{y\} \to \{z\}

Again, you get ∃xP(x,z). So, I’ve described two maps from B({x,y}) to B({z}) that should be equal. However, apparently the framework we’ve got does not yield this! Our notation makes the equality look inevitable, but it seems that’s not true. We need our functor B to obey the Beck–Chevalley condition, to get substitution and existential quantifiers to ‘commute’ with each other in a suitable sense.

Luckily, the Beck–Chevalley condition has a nice category-theoretic meaning: I’ve run into it in completely different contexts, like topological quantum field theory! But it’s still a bit mysterious to me.

Apparently we also need something else: Frobenius reciprocity. This gives us things like

y(P(xQ(y))   =   P(x) ˄ ∃yQ(y)

In other words, we can pull a conjunction out of an existential quantifer if the predicate involved, here P(x), doesn’t involve the variable we’re quantifying over.

So, my question now is: do you want to dig into these issues, or should we just assume someone has worked them all out?

MW: Yikes! The Beck-Chevalley and Frobenius conditions look like heavy-duty categoriosity. I think I’m ready to move on to applications.

JB: When you say that the Beck–Chevalley condition and Frobenius reciprocity are “heavy-duty”, you just make me want to explain them. They’re not that bad!

For example, Frobenius reciprocity just says that for any function f between finite sets, the left adjoint of B(f) preserves products. Right adjoints always preserve products, but if a left adjoint preserves products that’s worth writing home about!

But what does this mean for logic? A Boolean algebra is a category, and the product in this category is “and”. The left adjoint of B(f) often involves existential quantifiers. So Frobenius reciprocity gives rules like this:

y(P(xQ(y)) = P(x) ˄ ∃yQ(y)

See? We’re pulling an “and” out of an existential quantifier.

We don’t need anything fancy like Frobenius reciprocity to get this:

y(P(xQ(y)) = P(x) ˄ ∀yQ(y)

Since a universal quantifier comes from a right adjoint, this rule will hold automatically in our categorical setup.

So none of this is extremely stressful. But like you, I’m eager to move on to applications.

MW: But first I want to make sure I follow what’s going on. Our two favorite functors B: FinSet → BoolAlg, Bform and Brel, satisfy the Beck–Chevalley condition and Frobenius reciprocity, right?

JB: Right. I tried to persuade you that these extra conditions are familiar laws of logic, which hold in every example of type Bform. I also pointed out that every example of type Brel is isomorphic to one of type Bform: you just cook up a theory in first-order logic with an n-ary predicate P for each n-ary relation on your chosen set V.

MW: But an arbitrary functor from FinSet to BoolAlg might not obey these extra conditions?

JB: I guess not.

MW: Oh yeah, not an arbitrary functor, but one satisfying all this adjoint stuff we’ve been discussing. Let’s call it an adjointful functor.

JB: Right. It must be possible for an adjointful functor B: FinSet → BoolAlg to fail to obey Beck–Chevalley and Frobenius, or obey just one of these conditions yet not the other. Otherwise, why would they impose both these extra conditions? These category-theoretic logicians aren’t stupid! But I haven’t seen counterexamples yet. I’ll have to find some.

MW: Also, people are convinced that adjointfulness and Beck–Chevalley and Frobenius are all we need to demand of B. Why? Some sort of representation theorem? Maybe, any such functor is naturally isomorphic to an instance of Bform?

JB: Actually this should be straightforward. Just take the usual laws of first-order logic with equality, and show they hold for any adjointful functor B: FinSet → BoolAlg obeying Beck–Chevalley and Frobenius. That means these laws are enough. To show they’re not too much, take the entire definition of “adjointful functor B: FinSet → BoolAlg obeying Beck–Chevalley and Frobenius” and see what it says for our example Bform. We did a few pieces of that exercise. But if we did it thoroughly, we could show that all we get are familiar laws of first-order logic with equality.

None of this can possibly require any cleverness. Persistence must suffice. The upshot will be a representation theorem of the sort you describe: every functor B obeying all these conditions is naturally isomorphic to a functor Bform: that is, one coming from a theory in first-order logic with equality.

Someone should have done this, but I don’t know where.

By the way, we don’t need to require both left and right adjoints. If you have left adjoints, you get right adjoints for free, and vice versa! The reason is that we’re working with Boolean algebras, which are isomorphic to their opposites. In more logician-friendly lingo, what I’m saying is that

∀ = ¬∃¬

This is true in classical logic; in intuitionistic logic, which category theorists often favor, it’s not. They use Heyting algebras instead of Boolean algebras.

It’ll be trickier to show that Beck–Chevalley and Frobenius are both actually needed: that you can’t derive either from the other in the presence of adjointfulness. To do this, I might look for some counterexamples. I’ll work away at this in my spare time, or break down and ask people on the n-Category Café.

But for now, let’s move on to some applications.

MW: Onward to Gödel completeness!

Leave a comment

Filed under Categories, Conversations, Logic

First-Order Categorical Logic 3

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

Non-standard Models of Arithmetic 11

MW: Time to start on Enayat’s paper in earnest. First let’s review his notation. M is a model of T, a recursively axiomatizable extension of ZF. He writes \mathbb{N}^M for the ω of M equipped with addition and multiplication, defined in the usual way as operations on finite ordinals. So \mathbb{N}^M is what he calls a T-standard model of PA.

Continue reading

1 Comment

Filed under Conversations, Peano arithmetic

Non-Standard Models of Arithmetic 10

(MW: I have converted the first few posts into pdf files, formatted both for a small screen screen and a medium-sized one.)

JB: So, last time you sketched the proof of the Paris–Harrington theorem. Your description is packed with interesting ideas, which will take me a long time to absorb. Someday I should ask some questions about them. But for now I’d like to revert to an earlier theme: how questions about the universe of sets cast their shadows down on the world of Peano arithmetic.

Continue reading

1 Comment

Filed under Conversations, Peano arithmetic

First-Order Categorical Logic 2

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

(A conversation beteween 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

Simple Sets and the Recursion Theorem

These notes on Simple Sets are a grabbag about the simple sets of recursion theory. If you don’t know what those are, you probably are not interested, but the Wikipedia article is nice and short and gives the basics.

The last result uses the “shiny black box” (see below), which seems like cheating, but isn’t!

I wrote up the notes sometime in the 1980s based on two papers, and on a lecture by Michael Stob at MIT (reporting on joint work with Maas and Shore). They discuss effectively simple sets and promptly simple sets.

Continue reading


Filed under Logic