To Categories!

One hot area of proof theory research is categorical semantics of proofs. For some, this abstraction may seem like needless faffing about. I'll admit that I used to think that myself. I'll try to convey the intuitions that led me to change my mind.

Traditionally, the way in which one obtains an algebraic model of a logic is to pass to the so-called Lindenbaum algebra of the logic. Let's look at that process for classical logic. The first step is to define an equivalence relation on the set of well formed formulas (wff's). If x and y are wff's then define the equivalence relation ~ by saying that x ~ y iff |- x <-> y. Letting [x] denote the equivalence class of x under this relation, we define a partial order on the set of equivalence relations by saying that [x] <= [y] iff x |- y. So we have a poset, which we can turn into a lattice in the obvious way by defining [x]&[y] = [x&y] and [x]v[y] = [x v y]. Why might this not be a good enough semantics for us? Well, the point is that the partial order only records the fact that there is some proof of x |- y -- that is, some deduction from x to y. Thinking topologically for a moment, suppose we have two points in a topological space. Then, the equivalent notion would be to say that there is a path from x to y. But, whether or not all paths are "equivalent" depends on the space!

Recall that given two paths f,g from x to y in some space, f and g are homotopic if they can be continuously deformed into each other. This is not possible if, for example, there is a hole between them. Merely recording the fact that there is a path does not capture this information.

So, one might try to do the same thing for logic. If you try to do it concretely, by defining actual topologies on the logic, then you'll find yourself getting into a bit of a tangle. In fact, I tried to do this for a while, before caving in and doing it via categories. Categories work much smoother!

The idea is that we build a category C whose objects are formulae and whose arrows are "equivalence classes of proofs" between formulae. Defining the equivalence relation in a reasonable manner is a tricky business. Looking a bit closer, take two formulae x and y and consider the set of all proofs from x to y (for the finicky category people out there, there is no real loss in making the category locally small). This is denoted Hom(x,y). If this is nonempty, then we can "look inside" and consider how the equivalence relation works out. One usually does this by proving cut elimination and then looking at cut-free proofs. I'll discuss a logic where this procedure works out in a really cool way from a mathematical standpoint in a later post.

But, why stop there? We may delve deeper into Hom(x,y) and look at procedures for sending one proof to another, just like a homotopy! In the current set up, this means that we would have a bunch of what are called 2-morphisms. These are fella's that send morphisms to morphisms. Sound heady? It's not. What we have done is to form a category whose objects are the sets Hom(x,y) and whose arrows are transformations of proofs. Thinking about this more would take us deep into the waters of n-categories, so I will leave that for another post.

Taking a step back and having a look at what we have done, we see that categorical semantics focus on proofs whereas traditional algebraic semantics focus on "mere" provability. There are some nice theorems that go via category theory to derive models for a logic which are complete in a very strong sense. That is, if two proofs are equivalent, then they are equivalent in every model and if they are not equivalent, then there is some model in which they are not equivalent. These "models" are usually built from some heavy duty mathematical gadgets.

Anyway, for those looking for a good survey of category theory as it applies to logic, check out:

Category theory for linear logicians. R. Blute, P. Scott.