That Logic Blog

June 07, 2005

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.


Anonymous Anonymous said...

This is something I was thinking about for a few days several years ago, and ended up deciding that this was just me trying to overapply category-theoretic formulations. I couldn't find any way to make use of the extra structure of a category as opposed to a partial order, which had already been well-explored. I suppose I didn't know enough about n-categories then (or now). Do tell us more! (I'll read that article too.) 

Posted by Kenny Easwaran

8:11 PM  
Anonymous Anonymous said...

I can't imagine how any reasonable person would ever think of category theory that "this abstraction may seem like needless faffing about". However, I have learnt that there are people out there so wedded to a set-theoretic view of the world that a categorial one is alien to them. The great Australian computer scientist Vaughan Pratt has had much of interest to say on this topic on the categories list.  

Posted by Peter

7:09 AM  
Anonymous Anonymous said...

The objection that many have to category theory doesn't really have much to do with foundations and set theory. In proof theory and computational logic more broadly, the focus has traditionally been on provability . Here, lattice-theoretic and universal algebraic techniques reign supreme and one probably won't get much of couching things in category theoretic language. It's only when one changes one's focus and worries about proofs that category theory starts to seem reasonable. So, I don't think it's a matter of seeing that the categorial view of the world is alien, so much as the fact that category theory only provides a different language for traditional questions of provability and not major new techniques. 

Posted by Jon

8:38 AM  

Post a Comment

<< Home