That Logic Blog

December 12, 2005

Kreisel vs Lawvere

(via Robert Seely on the categories mailing list). The slides should be interesting for anyone into foundations, category theory or both:


On 29 Nov 2005, the Montreal Category seminar hosted a talk by Jean-Pierre Marquis on the interaction between Kreisel's and Lawvere's views on category theory as a foundations for mathematics. It has been suggested that many on this list who were not able to attend the talk might find its contents of interest, and so would be interested to know that the slides for the talk are available on the triples seminar webpage, at
http://www.math.mcgill.ca/rags/seminar/

(scroll down to the talk itself - the direct link is here if you prefer). The slides are fairly complete, and give a good idea of the content of the talk itself.

Here is an abstract of the talk:

Jean-Pierre Marquis
Organization vs foundations: Kreisel, Lawvere and category theory

Abstract: it is well-known that in the nineteen-sixties, Bill Lawvere proposed that category theory could serve as a foundations for mathematics and logic. Only one logician reacted officially: Georg Kreisel. In a series of notes, appendices and reviews, Kreisel developed arguments against categorical foundations. In this talk, I will take a close look at his arguments, examine whether they are still convincing and propose that Kreisel's position is still underlying most of the arguments against categorical foundations heard to this day.

December 06, 2005

Polycategories


Say I have a sequent A,B,C,D |- E,F. I can picture this graphically as the diagram on the left. Squinting at it a bit, one may see it as a sort of a circuit, which maps the input wires A,B,C and D to the output wires E and F. Of course, as it stands, this is not a morphism, but we'll make it into one in just a sec.

Before doing that, let's think about composition. How can we compose two sequents? The answer, of course, is that we use cut. For instance, we could cut our sequent A,B,C,D |- E,F with the sequent F,G,H |- L,K,M to obtain A,B,C,D,G,H |- E,L,K,M. It's easier to think of this geometrically, as in the diagram on the right.

Let's try and make these diagrams mathematically respectable. To do so, we'll generalise the notion of a category. Normally, a category consists of a bunch of objects, together with maps that go between objects. For our generalisation, we'll take lists of objects and maps between these lists. After doing the obvious things in order to ensure that everything is kosher, what we end up with is something called a polycategory. For instance, we generalise morphisms between objects, to polymorphisms between lists of objects. Just as we have functors between categories, we have polyfunctors between polycategories. These do what you expect. Say A and B are polycategories and F:A -> B is a polyfunctor. Then, each object a of A gets sent to F(a) and every polymorphism f: a1, a2, ..., an -> aa1, aa2, ..., aam gets sent to F(f):F(a1), F(a2), ..., F(an) -> F(aa1), F(aa2), ..., F(aam). Well, to be honest, defining composition of polymorphisms is slightly tricky. But not too tricky - we just use cut!

It is clear that we can view sequents as polymorphisms in the evident polycategory generated by the ambient deductive system. And composition becomes easy to understand if we draw polymorphisms as boxes with wires!

But wait, I promised that we would turn these diagrams into morphisms, not polymorphisms! How to do this? What we need to do is to recall that the comma in a sequent is really just a proxy for conjunction on the left and disjunction on the right. So, a sequent A,B,C |- D,E is really the same as A ⊗ B ⊗ C |- E ⊕ F. I'm using ⊗ for conjunction, because it is easier to talk about this stuff with a multiplicative conjunction, which is really just a tensor product. Similarly, disjunction is represented as ⊕ - direct sum! Both of these are examples of monoidal structures on a category. In fact, we can add it to a category too. It turns out that, in a well defined sense, adding ⊗ and ⊕ to a polycategory is a conservative extension. Let's name these things ⊗⊕-polycategories.

We're not quite all the way to viewing the boxes as morphisms in some category. What is missing is something that tells us how ⊗ and ⊕ interact. So, we need to make sure that they play nicely with each other, by saying that there is a natural transformation from A ⊗ (B ⊕ C) to (A ⊗ B) ⊕ C and, dually, there is one from (A ⊕ B) ⊗ C to A ⊕ (B &otimes C). After throwing in these natural transformations and writing down some sensible commutative diagrams, we get what is known as a weakly distributive category.

Here's the cool part. The 2-category consisting of all ⊗⊕-polycategories is equivalent to the 2-category consisting of all weakly distributive categories. With less jargon, polycategories and weakly distributive categories are essentially the same thing! Neato! So, I have kept my promise. The first box is a morphism from A ⊗ B ⊗ C ⊗ D to E ⊕ F in some weakly distributive category. If you want to see how to prove this, plus a bunch of other cool results, look no further than:

Weakly distributive categories; J.R.B. Cockett and R.A.G. Seely

I can't resist pointing to the world's coolest application of polycategories. This is sort of a continuation of something I wrote about a while ago. Namely, it is an application to causal quantum evolution in physics. The basic idea is that we can view a system of interacting quantum systems as a directed acyclic graph, where the nodes are subsystems and the edges represent the causality relation. From this, we can go ahead and derive a polycategory in a straightforward way. Then we can do all sorts of cool things like whacking on some hilbert space representations, density matrices and the like in order to describe the system. I could go on about this, but instead I'll just point to the relevant paper, since everything is explained beautifully in it!

Discrete quantum causal dynamics; Richard F. Blute, Ivan T. Ivanov and Prakash Panangaden.

Update: Weakly distributive categories tell us all about how to use polycategories to model the multiplicative fragment of linear logic. If you want to see how to deal with the additive fragment, including a neat application to concurrent processes, you should check out:

SigmaPi-Polycategories, additive linear logic and process semantics; Craig Pastro