The n-Category Café

I need to reply to Todd and Robin’s important comments on cut elimination and symmetric monoidal closed categories, but it’s late, and I’m tired, and for now I just feel like saying a bit more about Kummer’s thoughts on prime ideals and fluorine, and Coquand’s talk… in part because what I’ve said so far was so sketchy it must seem almost deranged to someone who hasn’t thought about this stuff before.

Suppose we have a set of ‘kinds of atoms’: for example, the usual kinds of atoms you see on the periodic table. These freely generate a commutative monoid $M$. Every molecule or collection of molecules determines an element of $M$.

But, it’s possible that at some stage in the development of chemistry, only certain guys in $M$ will have been observed in nature! For example, until quite late in the history of chemistry, nobody ever saw fluorine except in molecules containing other elements.

So, there is a subset $I \subseteq M$ consisting of ‘observed collections of atoms’. And, it’s quite reasonable to assume this is a submonoid.

So, there’s an interesting math problem: given a monoid $I$ that is a submonoid of some free commutative monoid, find some free commutative monoid $M$ containing $I$.

The solution to that problem is far from unique. But in fact, we want to find some $M$ that’s the ‘smallest’ free commutative monoid containing $I$. For example, in our chemistry example, we can always enlarge $M$ by positing extra never-observed atoms… but that would be useless! On the other hand, real-world chemists sensibly postulated the existence of fluorine before ever seeing it, because it was one of the generators of the ‘smallest’ free commutative monoid $M$ containing the observed $I$.

This business of finding the ‘smallest’ free commutative monoid $M$ for a given $I$ is closely related to the study of monomial ideals in polynomial algebras — that is, ideals generated by polynomials. After all, free commutative monoids map to polynomial algebras under the ‘free vector space on a set’ functor. In the paper I just linked to, you’ll see some charismatic ways of drawing monomial ideals.

(However, monomial ideals are in 1-1 correspondence, not with general submonoids of a free commutative monoid, but to submonoids $I$ with $I M \subseteq I$. This extra property simplifies things immensely, but is not typical in the examples from chemistry. For example, once upon a time, chemists could get ahold of hydrogen fluoride, but not hydrogen and two fluorine atoms.)

Anyway, Coquand takes these ideas and goes in a different direction, more related to logic… but now it’s bed time.

—
There’s a talk by Thierry Coquand that mentions Kummer, prime ideals, fluorine and cut elimination, all together! They’re a lot more deeply related than I thought!
—

Thierry taught me these ideas a couple of years ago. They may be seen as a partial realization of Hilbert’s program to (mechanically) eliminate ideal object’s from mathematical proofs. Hilbert tried to use such an elimination to justify the use of these ideal objects and of non-constructive proofs. These ideas are developing in all kinds of directions and I am still trying to see the full scope of them (and combine them with my own). Thierry used cut elimination to obtain proofs of various Stone and Gelfand dualities. We recently used this to obtain Gelfand duality for C*-algebras valid in any topos. These ideas may be seen as concrete versions of the fundemental work by Banachewski and Mulvey who again used logical methods (Barr’s theorem) to generalize
Gelfand’s theorem to Grothendieck toposes. We discussed these ideas before.
Hilbert’s program is also crucial in our work on topos theory in quantum mechanics.

Bas

Bas wrote:

Thierry taught me these ideas a couple of years ago.

Cool! Could you say what some of the basic ideas are, in very simple terms? I think there are some very simple big ideas lurking around here, which could be explained with almost no jargon… but I don’t quite see what they are.

Coquand mentions the Nullstellensatz. Behind the Nullstellensatz there seems to be some idea like “If you can’t derive a contradiction of a specific form from assuming that a bunch of polynomials has a simultaneous solution, then there must be a solution”. Which is like saying “If you can’t derive a contradiction from some axioms, these axioms must have a model.”

In general, in the absence of any other machinery, if someone handed me some axioms that led to no contradictions, and told me to find a model of them, I’d try building this model syntactically… since what else could I do?

For example, this is how people invented the complex numbers. They posited $\sqrt{-1}$, and noticed you could play around with it and never get in trouble… so, they were able to ‘create’ the complex numbers in a purely syntactical way, as expressions of form $a + b \sqrt{-1}$.

The Nullstellensatz seems deeper, because you’re not just making up new numbers to solve your system of polynomial equations: you’re finding solutions using the existing number system. I guess the Fundamental Theorem of Algebra is the basic result of this type.

But what does cut elimination have to do with any of this? Coquand writes: “Introduction to some recent developments in constructive algebra and abstract functional analysis. This approach can be seen as an application of some basic results in proof theory: the main one being the completeness of cut-free provability. It can also be seen as a partial realisation of Hilbert’s program and uses the idea of ‘replacing’ an infinite object by a syntactical one: a logical theory which describes this object. It has close connections with formal topology: cut-elimination can be expressed as forcing/topological model over a formal space.”

But what does this really mean? I wish I understood it.

Could there actually be some significance to what at first seems like a mere pun: the relation of ‘ideals’ to ‘ideal objects’? Coquand’s talk seems to relate the two.

(I guess I’ve already seen that a ‘point at infinity’ — a classic example of an ‘ideal object’ — can be an ideal in a $C^*$-algebra.)

I thought it was very standard. Certainly if you leave off the word “intuitionistic” and talk about MLL, then you will find a lot more references, and just about all that I am aware of take the primitives to be $\otimes$, $\neg$, $\wp$ (this funny ‘par’ connective, De Morgan dual to $\otimes$), with constants $\top$ and $\bottom$ (units for $\otimes$ and $\wp$ respectively). In particular, no modalities ! and ?; if those are included, people generally say ‘MLL + exponentials’ or something similar.

I’m not sure what the best reference for the system MILL (as we know it) would be. But I too am surprised by their inclusion of !; I honestly think you’re on safe ground sticking to your guns here.

No, actually, I think that’s the Deep Magic here. The cut rule doesn’t inline the proof.

I think this is the right analogy (please, logicians, smack me if I’m wrong). You could write a procedure in a C program called square:


float square(float x)
{
return x*x;
}


And then you could find the squared length with:


float squaredlength1(float x, float y, float z)
{
return square(x)+square(y)+square(z);
}


This way of doing things is like using the cut rule. The Cut Elimination Theorem tells us that there’s another way of writing this function that doesn’t use a subroutine call:


float squaredlength2(float x, float y, float z)
{
return x*x+y*y+z*z;
}


Is that more or less accurate?

It’s \multimap.

Thank you!

I’m trying to understand: we’ve got a symmetric monoidal closed category $A$, and we “interpret it in $B$” by taking a symmetric monoidal functor $F: A \to B$. Then we use the fact that $B$ is equivalent to its skeleton $C$; calling that equivalence E, we get $E F: A \to C$. Then we pull the monoidal structure on $C$ back to $A$ to get the comma. Is that right?

Sorry; I didn’t mean to be so terse or cryptic. I had something slightly different in mind.

One can think of the sequent calculus for MILL as giving a means of presenting the free symmetric monoidal closed categories $F[X, Y, Z, \ldots]$ (generated by a set or discrete category of positive literals $X$, $Y$, $Z$, …). The objects of the free structure are MILL formulas, and the morphisms $A \to B$ are equivalence classes of MILL-valid deductions of sequents $A \vdash B$. So the question I was trying to give an answer to was: what would the corresponding meaning of equivalence classes of MILL deductions of more general sequents $A_1, \ldots, A_n \vdash B$?

One answer has already been suggested: that these equivalence classes of deductions could be considered the multimorphisms of a certain multicategory; actually the “underlying” multicategory of the free structure $F[X, Y, Z]$ (as a monoidal category). For details on this underlying multicategory construction, see Tom Leinster’s book, page 84 (his $V^\prime$ functor). But since your intended audience might not be familiar with multicategories (and you might not want to get into all that), I was suggesting slightly different language with essentially the same content.

Namely, there’s a way of formally “strictifying” a monoidal category $M$ to get a strict monoidal category $M^\prime$ monoidally equivalent to $M$. I believe the construction is given by Joyal and Street in their Geometry of Tensor Calculus paper (and it can also be extracted from Tom’s discussion). The objects of $M^\prime$ are finite lists of objects of $M$. Then, to each finite list $\Gamma = A_1, \ldots, A_n$ one can associate a “clique” which is the diagram of all ways of tensoring up the $A_i$ in order, possibly with copies of $I$ thrown in, and isomorphisms between them based on the monoidal structure in $M$. (One thinks of each $n$-fold tensoring as tagged by a planar tree $\tau$ with $n$ leaves – a “classical tree” in Tom’s language, where each node has 0 or 2 incoming edges corresponding to the unit or an application of tensor. The tensoring itself might be denoted $\otimes_\tau \Gamma$. Then, given two trees $\tau$ and $\tau^\prime$, Mac Lane’s coherence then specifies a well-determined isomorphism $f_{\tau, \tau^\prime}: \otimes_\tau \Gamma \to \otimes_{\tau^\prime} \Gamma$ between the two tensorings in $M$.)

Then, a morphism $\Gamma \to \Delta$ in the strictification $M^\prime$ is just the obvious notion of clique morphism: a collection of maps in $M$ of the form

$$\phi_{\tau, \sigma}: \otimes_\tau \Gamma \to \otimes_\sigma \Delta$$

(ranging over trees $\sigma$, $\tau$) which are compatible with all the $f_{\tau, \tau^\prime}$, $f_{\sigma, \sigma^\prime}$ in the sense of making all the triangles commute. For example, $f_{\tau, \tau^\prime}$ followed by $\phi_{\tau^\prime, \sigma}$ yields $\phi_{\tau, \sigma}$. These equations mean that the whole collection of $\phi_{\tau, \sigma}$ is determined by any single one of them; the device of cliques is just a way of ensuring that no way of tensoring is favored over any other; it’s completely egalitarian.

Hopefully it’s clear the way in which $M^\prime$ becomes strict monoidal; on objects the tensor product is concatenation of lists. $M$ is embedded inside $M^\prime$, where objects are interpreted as lists of length 1. If you think a little further about it, this embedding is a monoidal equivalence (for example, any object $\Gamma$ is isomorphic to an object of $M$, namely to any of its tensorings $\otimes_\tau \Gamma$). So, that’s the formal strictification.

Hence, (equivalence classes of) deductions of sequents $\Gamma \vdash A$ can be interpreted as morphisms $\Gamma \to A$ in the monoidal strictification of the free symmetric monoidal closed category. You and John are doing something slightly different from free structures in your hom-set approach, but that can also be adapted to this strictification interpretation of sequents (if you want).

Also, I’m sure I don’t understand cut elimination: the wikipedia page says that if you have proofs of sequents $A \vdash B$ and $B \vdash C$, then anywhere in a proof of $A \vdash C$ mentioning $B$ you can inline the proof of $B$ instead. But isn’t that just what the cut rule does!?

Sadly, I’m not the right person to ask since I don’t speak “programming” (I think Robin does though). I have a sense of what this inlining business is saying, and I think John Armstrong’s response is in the right spirit, but my attempt to speak the lingo would be inarticulate – let Robin or someone else answer.

But maybe I can point you to a special but critical case of the cut-elimination algorithm for MILL which I hope helps. Go to Proofs and Types, page 106, and look at case 6, where one cuts at the formula $C \Rightarrow D$. (Girard et al. are dealing with classical = non-intuitionistic sequents; to remove clutter and put yourself in MILL, take $\underline{B}$ and $\underline{B^\prime}$ to be empty, and $\underline{B^{\prime\prime}}$ to be a singleton.) Here the deduction (which ends with cutting at $C \Rightarrow D$) is replaced by a deduction involving two cuts, one at $C$ and one at $D$. So in effect, in cut-elimination, applications of cut are pushed back to simpler and simpler formulas until one pushes them all the way back to the level of axioms (identities $X \vdash X$ on literals $X$), where they are at last eliminated (since composition with an identity does nothing). That’s the rough idea, although the careful multiple inductions are a little bit fussy – Proofs and Types gives plenty of detail.

Mike wrote:

I like to think of the comma as denoting the tensor product of the monoidal strictification of the smc category where these sequent deductions are interpreted.

I’m trying to understand: we’ve got a symmetric monoidal closed category $A$, and we “interpret it in $B$” by taking a symmetric monoidal functor $F:A\to B.$ Then we use the fact that $B$ is equivalent to its skeleton $C$; calling that equivalence $E,$ we get $E F:A \to C.$ Then we pull the monoidal structure on $C$ back to $A$ to get the comma. Is that right?

I don’t know where you got that ‘skeleton’ stuff from, but it makes me fear you’re succumbing to a classic beginner’s mistake: trying to make a monoidal category strict by making it skeletal.

In case you were making this mistake, let me say what it is, and what to do instead.

In a monoidal category we have an associator

$$a_{X,Y,Z} : X \otimes Y) \otimes Z \stackrel{\sim}{\to} X \otimes (Y \otimes Z)$$

Switching to a skeletal subcategory ensures that

$$(X \otimes Y) \otimes Z = X \otimes (Y \otimes Z)$$

but this doesn’t help at all if you’re trying to make the associator equal to the identity!

In fact, to make the associator equal to the identity, we need to go in the opposite direction. We need to throw in a lot more isomorphic objects.

The trick is to create a new category where objects are lists of objects in our old category, and define a new tensor product such that

$$(X_1, \dots, X_n) \otimes (Y_1, \dots, Y_m) = (X_1, \dots, X_n , Y_1, \dots, Y_m)$$

Then you can set the associator equal to the identity and see that this new monoidal category is monoidally equivalent to the original one!

This is the trick Todd is calling ‘monoidal strictification’, and in applications to logic, the commas are supposed to remind you of sequents.

So: if you want to make a monoidal category strict, don’t make it skeletal: add flab!

In the programming analogy: if the cut rule is like a function call, eliminating the cut corresponds to inlining the function.

As this analogy suggests, in practice it is not generally wise to eliminate all cuts from a proof: if you do, the size of the proof can blow up exponentially. George Boolos has a fun paper Don’t eliminate cut! which gives a simple example where this happens.

Yes, you’re right – you don’t really need Gentzen sequent calculus in order to prove a cut elimination theorem, nor do you particularly have to mention strictifications per se. What I really meant (and what I should have said) is that cut-elimination is above all a syntactic theorem which is sensitive to just how the syntax is presented.

To prove the point, Kelly and Mac Lane, in their famous paper Coherence in Closed Categories [JPAA 1 (1971), 97-140], proved a cut elimination theorem in purely categorical language – no sequents, no strictifications, no nuthin’. Roughly, they showed that each canonical transformation that is constructible in the theory of smc categories is one of four types (corresponding to the four ‘logical’ rules of MILL) – the crux is to show that the class of transformations of these four types is closed under composition. That’s their cut elimination theorem.

See, I don’t think they liked this Gentzen sequent business any more than most category theorists – as I found out, very quickly, when I began giving seminar talks on my thesis in Australia! [I myself find the ideas clearer when expressed in sequent calculus, but hey, that’s me.] But anyway, the point remains that the cut-elimination theorem is syntactic in nature and a bit sensitive to how the syntax is presented.

But I say let’s not worry about it. I think it would be quite enough just to say a few words on what sequents (as long as you’re talking about them!) are good for; maybe add for the sake of honesty that the way you’re presenting it is a slight simplification and not exactly the way (categorical) logicians do it for their purposes, but anyway you’re not trying to prove a theorem of logic for goodness’ sake! So yes, I think your hopes are confirmed.

Could I say it amounts to a decision procedure for telling 1) when a homset in a freely generated SMCC is nonempty and 2) when two elements of the homset, described syntactically in terms of certain basic ‘generators’, are equal?

Cut-elimination is in any event a crucial step toward such a decision procedure. The traditional concern of logicians was 1), the issue of provability of formulas or sequents. Of perhaps greater concern to category theorists and many others is 2): deciding if a diagram commutes.

And, by ‘freely generated’ do we only mean free on a set of objects, or can we throw in some extra generating morphisms as well?

First, let me say that I think you can probably soft-pedal this business of free structures (since it’s mathematical physicists you’re addressing), if you want, with words like “deciding when a diagram commutes on the basis of the axioms/commutative diagrams of the theory”, or something like that. But anyway, “freely generated” can mean on any category. If you have an oracle who can tell you when two arrows of a category $C$ are equal, then there’s a procedure for deciding equality in $F[C]$ relative to equality in $C$.

Have we talked about clubs and wreath constructions much at the Café? In fact, what Max Kelly showed is that the free structure $F[C]$ is equivalent to a kind of “wreath product” $F[1] \int C$. So really, “all” you need to know is the structure of $F[1]$ (where $1$ is the 1-object 1-morphism category); then, with the help of your $C$-oracle, you know all about $F[C]$. The same type of thing holds whenever the theory or doctrine is expressible as a so-called “club”.

The unit and counit of adjoint functors always satisfy certain zig-zag identities, and these should imply the zig-zag identities for i and e. But now you’ve got me worried.

Yes, this is precisely the right place to get a little worried. The idea is quite seductive, but it doesn’t seem to work out when you look at the details. Just try to do it, and you’ll see what I mean.

Suppose we have a natural isomorphism $\phi_{A,B,C}: \mathbb{C}(A\otimes B, C) \to \mathbb{C}(B, A*\otimes C)$, as in your definition. If you want the zig-zag identities to come out right, you need an extra compatibility condition. Specifically: ask that for any arrow $f: A\otimes B\to C$ and object $X$, we have $\phi(f\otimes X) = \phi(f)\otimes X$. (Of course you need to add some associators in there really; I omitted them to avoid clutter.)

Just to confuse things, I should add that I’ve never seen or heard of a category that satisfies your condition but is not compact closed, so it is possible that your definition is equivalent to the usual one after all. However, if it is true then it’s true for some as-yet unknown reason!

Wanting to get to grips with all this, I’ve read through the discussion above between Robin and Todd. It’s quite possible I’ve misunderstood something — as Todd says above, this is all somewhat subtle — but it seems to me that different people are talking about different things.

Todd says:

I had made a similar claim once here at the Café [that $(X \otimes −) \dashv (X^* \otimes −)$ implies compact closure], whereupon Robin contacted me privately and convinced me it ain’t necessarily so!

Assuming that Todd meant “$(X \otimes −) \dashv (X^* \otimes −)$ for all $X$ implies compact closure” — surely this is true! Just take the unit and counit of the adjunction at stage $I$, which witness the fact that $X$ is left-dual to $X^*$.

From these morphisms we can construct an adjunction $(X \otimes − ) \dashv (X^* \otimes −)$, and I thought that the long discussion above was about whether every adjunction $(X \otimes − ) \dashv (X^* \otimes −)$ is of this form, with unit and counit deriving from the unit and counit at stage $I$. (As Todd says above, “it suffices to show … that the counit and unit are given by what they do at I.”) This is interesting, but surely superfluous for the question of whether $X$ has a right dual.

Interesting! I feel rather embarrassed that I’m so ignorant of the history of these ideas. In fact, all I knew about Szabo’s book was that it had become mildly notorious for its mistakes, and I’ve avoided it for fear of being misled. It sounds as though I shouldn’t have.

Is Blute’s dissertation published or otherwise available?

Hey Todd, why don’t you put a copy of your thesis online? (Scanned, if there’s no other way.) The public demands it!

The hard part is proving cut-elimination – fortunately Gentzen did that for us in the 1930s – then the harder part is finding a minimal set of “commuting conversions” modulo which cut elimination preserves equivalence. (I don’t know who was the first to do that. I would guess Lambek, in the cartesian case?) Once you’ve done that, you can describe arrows of a free SMCC as proofs module commuting conversions.

Lambek for the cartesian closed case, I believe that’s right. I think it may be in one of those early Midwest Category Theory Seminars (in Lecture Notes in Mathematics). Earlier he also tackled monoidal biclosed categories without units, which he called “residuated categories”.

I believe Szabo (who was Lambek’s student) gives the complete set of commuting conversions (aka “Lambek equivalence relation”) for the sequent calculus of smc categories; if I recall correctly, the only mistake is the claim that according to the way he orders the local conversion rules (where one side is considered more normal than the other), that the result is a strongly normalizing and confluent algorithm for deciding Lambek equivalence. Had he been right, that normalization procedure would have solved the relevant coherence problem.

I like Schalk’s notes! But: in the rules for MILL in Table 1, is there also an ‘exchange’ rule missing, corresponding to the symmetry of the symmetric monoidal category? Or is that somehow implicit?

I’d like to refer to these notes. Does it make sense to try to get mistakes fixed?

In Section 1.3.3 you give some axioms, but I’d like to see how those axioms could be satisfied in a familiar situation, and in particular what the equivalence relation would be.

Section 1.3.2 seems to start out with concrete propositions and proofs, so I was hoping that in this section you might define the equivalence relation.

But now that I think about it, maybe it’s clear: do you just take the coherence equations that hold for the braiding iso, identity iso, etc. and use them to generate the equivalence relation?

Dan wrote:

But now that I think about it, maybe it’s clear: do you just take the coherence equations that hold for the braiding iso, identity iso, etc. and use them to generate the equivalence relation?

Right, that’s the idea. Since it wasn’t instantly obvious, I need to explain it better. It’s great getting feedback from logicians, but it’s also great getting feedback from non-logicians, since they’re the folks we’re actually trying to talk to here.

By the way, I’d also love you to look over the section on computation, as soon as that’s fit for human eyes. I’ll do another blog entry on that in about a week!

I understand your concerns. Nevertheless, it’s probably a bad idea to use the word “classical” the way physicists use it when you are going to talk about logic. Since you never ever have to distinguish between classical and intuitionistic logic, you could just avoid the question whether to confuse physicists or logicians with a bit of careful wording.

You are right, there is probably little point in explaining the difference between propositional and predicate calculus. Maybe, for the benefit of those who do know the logical terminology, you can throw out the relevant phrase at some point. I was confused when I read the text. My first thought was “gee, they mixed up things” because I did not think of the physicist’s point of view (classical vs. quantum).