# linear logic, diagrammatic calculus and foundations

Hi,

I have been interested in foundations for a while, especially categories as foundations. I am of the opinion that, as long as we present the theory of categories in SET, we will not be able to give a reasonable justification for categories as a foundation. (that could be a question: does the persistent presentation of the theory of categories in SET preclude it from taking its place as a foundation?)

How else can we present the theory of categories?

What, in your mind, is a foundation anyway? To me, it is a way to express ideas (language with syntax or diagrammatic calculus or other mysterious thing) and have reasoning that we all agree on because it has precise rules.

My next question is about how to present the theory of categories in a linear logic. I am working on a few intuitions about how to have such a thing. First is the intimate link between linear logic, and the geometry of tensor calculus. Second, we normally think of the geometry of tensor calculus as being only about one particular kind of category. However, the basic reasoning in GTC is about planar graphs. Categories are exactly planar graphs with extra data over the edges. Thus, GTC is also a place to reason about categories in general, not just a particular brand of category.

Is it possible to present the theory of categories in a linear logic and would this presentation not be more of a diagrammatic presentation? GTC comes with a calculational tool. It is a diagrammatic calculus.

Swapping morphisms for arrows in categorical diagrams was a huge turning point for physics: See Markopolou and also see Panangaden, Blut, Ivanov and see Coecke,Abramsky. This swap opened up the diagrammatic calculus. Maybe we should feed this simple change back to category theory as a means of making it more of a foundation.

-
In what sense are categories "exactly planar graphs with extra data over the edges"? The usual way of drawing categories as graphs --- a vertex for each object and edges for the morphisms (or at least for enough morphisms to generate the category) --- need not be planar, even if the graph is finite. And for some categories, the graph will have more vertices than there are points in the plane. – Andreas Blass Jun 23 '11 at 18:08
The "data" can be universal statements like "For every edge e, there is an edge g, s.t. eg=Identity. This is how we have data over many edges without listing the data. – Ben Sprott Jun 23 '11 at 18:18
Andreas, thanks for the input. Can I have an example of the category which is not planar? I realize I am beyond my limit in terms of understanding, but would you wager a guess as to whether or not this precludes a linear logic presentation of the theory of categories? ...That is, if you think that question even has meaning. – Ben Sprott Jun 23 '11 at 19:13
@Ben take a non-planar finite graph. Take the free category on that graph. The graph underlying this category contains the original graph, so is not planar. – David Roberts Jun 23 '11 at 22:57

Just to address one of the issues raised by the questioner: the formal theory of categories does not depend on $Set$, any more than the formal theory ZFC depends on $Set$ (what would the latter even mean?). It's just a first-order theory. One formal syntactic presentation of it can be found here; there is no mention of $Set$ or "collection" or anything like that.

Naturally, the conventional mode of presentation involves words like "a category consists of a collection $C_0$ of objects, and collection $C_1$ of morphisms", etc., etc. This is usually done at a pre-formal level, and has the advantage of readability. It's a kind of pre-formal semantics where the word "collection" is left unanalyzed. If one goes further, and demands that "collections" be sets which are elements of a structure $(V, \in)$ satisfying some set-theoretic axioms such as ZFC, then ultimately one is giving the notion of an interpretation of the theory of categories in the theory ZFC. But the formal first-order theory of categories, insofar as it is given syntactically, stands perfectly well on its own, as does the theory of ZFC. There is no dependency in either direction.

(Of course, category theory manifestly refers to set theory wherever it uses words like "small" and "locally small", but this is a different issue.)

The amount of first-order logic needed to express the theory of categories is small: in the jargon, the data and axioms are "essentially algebraic" (i.e., they can be given in terms of a sequence of operations where the domain of each partially defined operation can be specified in terms of equations involving previous operations). This means that "internal category objects" need very little ambient structure to express them: they can be defined in any category with finite limits. The theory ZFC needs much more first-order logic, and correspondingly much more ambient structure to interpret it internally.

If you want to beef up the theory of categories to a "foundational theory" which will serve the needs of most mathematicians, one has various options. Among them is ETCS (see the page I liked to above for the formal theory), which is weaker than ZFC but probably suffices for most purposes.

I am not sure what you mean by giving the theory of categories within linear logic. If you mean multiplicative linear logic, you will have to deal with the axioms that involve the contraction and weakening rules for conjunction, which one doesn't have in MLL.

Added: as far as diagrammatic presentations are concerned, you might be interested in the Q-sequences of Freyd, as discussed in the book Categories, Allegories.

-
Todd, what about quantum categories a la Day, Street etc.? – David Roberts Jun 23 '11 at 23:00
Regarding structural foundations using 'smallness' without an ambient set theory, Benabou had ideas on this by replacing the codomain fibration $Set^\to \to Set$ by a fibration with a class of maps. encoding smallness, called by him a 'calibration'. This class is 'just' a saturated singleton Grothendieck pretopology. I'm not sure how this relates to algebraic set theory, which I'm sure as you know, Todd, postulates the existence of a category of classes and 'small maps', which are essentially those with sets for fibres (IIRC). – David Roberts Jun 24 '11 at 1:10
I think I just need more clarification as to what Ben wants; I can't quite tell from the post. One can of course simulate contraction and weakening in, say, a symmetric monoidal category, by passing to the category of commutative comonoids therein, where the tensor product becomes cartesian product. Similarly, in full linear logic, there is a symmetric monoidal comonad $!$ whose values $!A$ carry suitable commutative comonoid structures. I'm not up on quantum categories; is there is a similar idea there? Anyway, as I said in my answer, I'm not sure what Ben is after. – Todd Trimble Jun 24 '11 at 1:18
Regarding your second comment: quite right, David. There are a number of devices for incorporating smallness structures in formal theories of categories; another is given by the concept of yoneda structures. Thank you for reminding me of this! I think I was writing a little too quickly... – Todd Trimble Jun 24 '11 at 1:23
I want to thank everyone for the great responses. – Ben Sprott Jun 24 '11 at 14:01