Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

February 21, 2008

Logicians Needed Now

Posted by John Baez

Mike Stay and I are writing a paper for a book Bob Coecke is editing: New Structures for Physics. The deadline is coming up soon, and we need your help!

We’d really love comments on the ‘logic’ section, because neither of us are professional logicians. I haven’t included the ‘computation’ section in this draft, since it’s embarrassingly far from finished… but Mike knows computation.

You’ll probably notice if you take a look at this draft: we’re not trying to give a conventional treatment of proof theory… we’re just trying to sketch how a few ideas in that subject are connected to category theory. So, we expect that what we say will sound weird and sort of superficial to expert logicians. But, we don’t want to say anything too embarrassing!

In particular, we only discuss an incredibly impoverished form of the propositional calculus, without ‘or’ or ‘false’. This is because we’re only trying to discuss what can be done in a symmetric monoidal closed category… the paper is long enough just doing that! We can’t get into the richer categorical structures beloved by logicians.

Worse, we never mention sequents like this:

A 1,,A nB A_1, \dots, A_n \vdash B

We only mention these:

AB A \vdash B

As Jon Cohen pointed out, this means our inference rules lack the ‘subformula property’: namely that every formula about the line is a subformula of some formula below the line.

Alas, I don’t know what to do about this problem without significantly modifying our setup. Josh mentioned multicategories as one approach, but I have no idea how this would work for the ‘quantum logic’ systems our setup is designed to include. So, I guess I’ll just mention the problem.

In a way it doesn’t really matter, since we’re just trying to set up tenuous bridges between various subjects… just enough to get more people talking to each other. But, it’s good to know about the hot water we’re getting into.

Posted at February 21, 2008 3:03 AM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1607

84 Comments & 3 Trackbacks

Re: Logicians Needed Now

You probably know that chemistry (p. 35 of your paper) and logic have been related before. I recall Charles Peirce writing on this. More recently we have the chemical abstract machine.

Hmm, the connection goes back at least as far as Hegel.

Posted by: David Corfield on February 21, 2008 11:34 AM | Permalink | Reply to this

Re: Logicians Needed Now

David Corfield:

You probably know that chemistry (p. 35 of your paper) and logic have been related before.

I’d forgotten this, though now I seem to recall you mentioning it. Thanks — that’ll make a nice touch of erudition!

(I wonder if other people explaining linear logic have mentioned the analogy to chemical reactions: it seems pretty obvious, but I haven’t seen it in that context before.)

Now I’m reminded of how Kummer compared ‘ideal numbers’ to the element fluorine, whose existence was only known indirectly at the time, because it hadn’t been isolated: it existed only in combination with other elements.

Hey!

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!

He says:

Prime ideals were introduced by Kummer by analogy with chemistry. “These ideal complex numbers are comparable to hypothetical radicals that do not exist by themselves, but only in their combinations.” Kummer gave an example of an element (fluorine) that, at the time, existed only hypothetically comparable to a prime ideal (this element was isolated later).

But then he goes much deeper, showing how the Nullstellensatz and related results in algebra are connected to proof theory and ultimately (though I don’t understand this yet) Gentzen’s cut elimination theorem!

Interesting bunch of ideas!

Posted by: John Baez on February 22, 2008 4:51 AM | Permalink | Reply to this

Re: Logicians Needed Now

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 MM. Every molecule or collection of molecules determines an element of MM.

But, it’s possible that at some stage in the development of chemistry, only certain guys in MM 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 IMI \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 II that is a submonoid of some free commutative monoid, find some free commutative monoid MM containing II.

The solution to that problem is far from unique. But in fact, we want to find some MM that’s the ‘smallest’ free commutative monoid containing II. For example, in our chemistry example, we can always enlarge MM 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 MM containing the observed II.

This business of finding the ‘smallest’ free commutative monoid MM for a given II 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 II with IMII 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.

Posted by: John Baez on February 22, 2008 7:44 AM | Permalink | Reply to this

Re: Logicians Needed Now


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

Posted by: Bas Spitters on February 22, 2008 10:26 AM | Permalink | Reply to this

Re: Logicians Needed Now

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 1\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+b1a + 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 *C^*-algebra.)

Posted by: John Baez on February 22, 2008 8:09 PM | Permalink | Reply to this

Re: Logicians Needed Now


Cool! Could you say what some of the basic ideas are, in very simple terms?

I’ll try to say a few things.

A geometric theory, one using only finite conjuction and arbitrary disjunction, describes a topological space, its Lindenbaum algebra, or syntactic category. This is a locale, or complete Heyting algebra. As you know a locale is a generalization of a topological space. We do not insist that the Heyting algebra is an algebra of sets. The points of a locale are its complete prime filters. These points correspond to the models of the geometric theory.

Often these points are “constructed” using non-constructive methods: the axiom of choice for instance. Consider the Gelfand spectrum of a C*-algebra. There one uses the axiom of choice to “construct” the points. However, these points are almost never needed in applications. The locale structure is what matters. Moreover, because the spectrum as a topological space is non-constructive it does not generalize to other toposes then Set. In applications where we have a continuous field of C*-algebras we need the localic version of the theorem. All of this leads to the idea that the use of the axiom of choice is a choice (it is not needed) and usually a bad choice (theorems obtained in this way do not generalize). Many of the standard applications of the axiom of choice in functional analysis have been removed in this way.

All of this may be seen as a shift from model theory, the existence of points, to proof theory, the locale is non-trivial. So, instead of proving that a point exists one proves that the corresponding theory is consistency. By an application of a non-constructive completeness theorem one goes from one to the other. However, this last move is not needed in practice. This is also what is going on in the Nullstellensatz. [When reading Tao’s post on this, I got the impression that his ideas may be related.]

Typically, when using these methods one did not analyse the corresponding constructive proofs, but was happy with their non-constructive existence, using a Goedel-style completeness theorem. Hence it gives a classical proof of the existence of a constructive proof. Surprisingly, once found, these constructive proofs are usually very elegant.

Thierry’s observation is that in case the space is compact Hausdorff. One can actually consider the finitary covering relation and hence have a finite proof system instead of the infinitary one used in geometric logic. This often allows one to extract very simple algebraic proofs from highly non-constructive arguments.

The connection between an ideal and an ideal element is very clear in the case of the Gelfand spectrum. The points/models are the maximal ideals, which require Zorn for its construction. Hence they are clearly idealized.

Finally, for the relation with cut-elimination: Suppose that we want to prove that something holds for all the points of the spectrum of a C*-algebra. Then, going to the logical side, this means that we want to prove that truth is derivable in the corresponding theory. In order to prove this it suffices to consider only cut-free proofs. This often makes it possible to find the very concrete proofs hidden in abstract arguments.

It’s time to go to bed…

Bas

Posted by: Bas Spitters on February 22, 2008 10:02 PM | Permalink | Reply to this

Re: Logicians Needed Now

Knowing almost nothing about much of the mathematics involved here (cut elimination) I risk a simpleminded comment.

“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?”

But syntactics, as in computer science, isn’t that just asking for what you want to be able to do (with a say a programming language), which is more or less what the axioms do already? Don’t you need a map to a concrete semantics, where the syntactical rules are implemented and where you can actually perform the calculations?

“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.”

This sounds very much like what a lazy functional programming language (like Haskell) does - but again in concrete semantics - the calculations can be done on a real computer.

Curious if these comments makes sense.

Posted by: Anders Bengtsson on February 24, 2008 8:20 AM | Permalink | Reply to this

Re: Logicians Needed Now

“This sounds very much like what a lazy functional programming language (like Haskell) does - but again in concrete semantics - the calculations can be done on a real computer.”

Indeed, Thierry Coquand also uses this analogy in the slides mentioned above.

Bas

Posted by: Bas Spitters on February 24, 2008 8:28 PM | Permalink | Reply to this

Re: Logicians Needed Now

Anders wrote:

Don’t you need a map to a concrete semantics, where the syntactical rules are implemented and where you can actually perform the calculations?

My point was that sometimes, when we’re desperate to find a model of some axioms, we resort to a “purely syntactical” model which is really just built from symbolic expressions.

For example, suppose I hand you the axioms describing a gizmo with one binary operation ×\times satifying the equations

a×b=b×aa \times b = b \times a

a×(a×b)=b×ba \times (a \times b) = b \times b

and I tell you to find some examples of such a gizmo — that is, some models for these axioms. You could look around for examples in nature, but this might be tough — except for the empty set or the 1-element set, which are always good things to try.

So, you might get desperate and start trying to build models syntactically. For example, you might say “how about the free gizmo on 3 generators xx, yy and zz?” This would have elements xx, yy and zz and also all formal products of them, like (x×z)×(z×x)(x \times z) \times (z \times x), modulo the relations imposed by the equations above. So, for example, x×(x×x)x \times (x \times x) would equal x×xx \times x.

Starting from these ‘free’ models, you can then build lots of other models using various constructions.

Using this sort of trick, we instantly know that any ‘algebraic theory’ — any theory describing a gizmo with a bunch of nn-ary operations satisfying equational laws — has plenty of models.

I was quite vaguely imagining using some trick like this in some other context…

Posted by: John Baez on March 1, 2008 6:33 AM | Permalink | Reply to this

Re: Logicians Needed Now

Alas, I don’t know what to do about this problem without significantly modifying our setup. Josh mentioned multicategories as one approach, but I have no idea how this would work for the ‘quantum logic’ systems our setup is designed to include. So, I guess I’ll just mention the problem. In a way it doesn’t really matter, since we’re just trying to set up tenuous bridges between various subjects… just enough to get more people talking to each other. But, it’s good to know about the hot water we’re getting into.

I think the subsection on proof theory will leave many scratching their heads about the point of it all, because here all proof theory appears to be is an especially cumbersome way of presenting the construction of proofs/morphisms.

To my mind, the crucial point underlying proof theory is that body of results that are called cut elimination theorems, which for a category theorist not accustomed to thinking of these things, says something quite incredible: that you can dispense with composition (your rule ()(\circ))!! That’s really a crude way of putting it, so let me say a bit more.

Imagine that you’re setting out to prove a difficult theorem, ABA \vdash B. Along the way you will need to prove a bunch of propositions which will get you from point AA to point BB: AA 1A \vdash A_1, A 1A 2A_1 \vdash A_2, …, A nBA_n \vdash B. (The cut rule, or rule ()(\circ), would then allow you to conclude ABA \vdash B.) In the case of a nontrivial theorem, there is no doubt that the intermediate formulas A iA_i could be quite complicated. If you actually wanted to mechanize the process (of deciding which A iA_i you will need), the problem would seem to be hopeless: the search space for the requisite intermediate formulas is infinite, unbounded. So having to rely on the cut rule would seem to be a very risky proposition, from that point of view.

Nevertheless, Gentzen and his successors showed that for deductive systems of carefully specified type, one can get around this fundamental difficulty: he proved a meta-theorem to the effect that any entailment (or sequent) ABA \vdash B that can be proven with the cut or composition rule, can also be proven without it! For example, as an application to the types of monoidal categories you and Mike are discussing in your paper, one can decide if there exists a morphism from one formula AA built up from \otimes and \Rightarrow (your lollipop connective – sorry, I don’t know the LaTeX code for that) to another BB, that is, a morphism built out of the data for the particular type of structured category being studied (monoidal, monoidal closed, symmetric monoidal closed, etc.). In effect, in the system left after the cut rule is removed, the only way one can infer an entailment or morphism below the line is by starting with entailment(s) above the line with a simpler logical structure. In a lot of such deductive systems which have been studied by categorists, the entailment ABA \vdash B one is after is built up from simpler ones, one connective at a time.

[There is also a more refined, categorified cut elimination, which allows one to decide not only if there exists a morphism ABA \to B, but whether two such morphisms built from syntactically different deductions are the same on the basis of the axioms (commutative diagrams) for the type of structured monoidal category being studied. This is the crucial step toward solving a coherence problem for that type of structure, i.e., deciding which diagrams commute. The fact that Gentzen cut elimination admits a categorified form is one of the great insights due to Lambek.]

But it should come as no surprise that to get away with a cut elimination theorem, one has to be very careful in just how the deductive system is set up – sometimes a delicate matter. In multiplicative intuitionistic linear logic (the logic for symmetric monoidal closed categories), the Gentzen method gives rules which introduce connectives one at a time, either on the left or right of the entailment symbol \vdash (the turnstyle). For example, there is a rule

Γ,A,B,ΔCΓ,AB,ΔC\frac{\Gamma, A, B, \Delta \vdash C}{\Gamma, A \otimes B, \Delta \vdash C}

which introduces a connective \otimes on the left (here Γ\Gamma, Δ\Delta denote lists of formulas). There is a separate rule

ΓA;ΔBΓ,ΔAB\frac{\Gamma \vdash A; \Delta \vdash B}{\Gamma, \Delta \vdash A \otimes B}

for introducing \otimes on the right. The various rules come in pairs like this, balanced “just so”, so that a cut elimination theorem can go through. In particular, I think one really does need sequents of the form

A 1,,A nBA_1, \ldots, A_n \vdash B

in order to get cut elimination to come out right. (Just FYI, the cut rule would take a form like

ΔA;Γ,A,ΣBΓ,Δ,ΣB).\frac{\Delta \vdash A; \Gamma, A, \Sigma \vdash B}{\Gamma, \Delta, \Sigma \vdash B}).

Multicategories are one semantic device for interpreting such sequents. Another is to think of the “commas” as the monoidal product for a monoidal strictification (a formal way of associating a strict monoidal category equivalent to a given monoidal category). I spoke a little about this back here; see also the comments which follow (including where Tom Leinster chipped in with a remark on unbiased monoidal categories).

I may have more comments later.

Posted by: Todd Trimble on February 21, 2008 4:06 PM | Permalink | Reply to this

Re: Logicians Needed Now

I’ll slowly work my way up to some more substantial issues, but for starters…

Todd writes:

In multiplicative intuitionistic linear logic (the logic for symmetric monoidal closed categories)…

Does anyone know how standard it is to use the term ‘multiplicative intuitionistic linear logic’ (or ‘MILL’) to mean precisely ‘the logic for symmetric monoidal categories’?

Right now about the only place I can find this usage clearly documented is in a paper by Hasegawa. Originally Mike and I used the term ‘MILL’ all over our paper — but then I got scared that it might mean different things to different people. For example, Benton, Bierman, de Paiva and Hyland seem to include the connective ! in their concept of MILL — see the rules listed on page 2.

Posted by: John Baez on February 23, 2008 5:30 AM | Permalink | Reply to this

Re: Logicians Needed Now

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.

Posted by: Todd Trimble on February 25, 2008 2:26 PM | Permalink | Reply to this

Re: Logicians Needed Now

Okay, good — thanks. Elsewhere the same Benton–Bierman–de Paiva–Hyland gang use the term ‘MELL’ (‘multiplicative exponential linear logic) to stand for the fragment of linear logic containing ,,\otimes, \multimap, \top and that exponential !. I like that better. So, I’ll stick to my guns.

Posted by: John Baez on February 25, 2008 8:14 PM | Permalink | Reply to this

Re: Logicians Needed Now

(your lollipop connective – sorry, I don’t know the LaTeX code for that)

It’s \multimap.

Back here you said,

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 AA, and we “interpret it in BB” by taking a symmetric monoidal functor F:AB.F:A\to B. Then we use the fact that BB is equivalent to its skeleton CC; calling that equivalence E,E, we get EF:AC.E F:A \to C. Then we pull the monoidal structure on CC back to AA to get the comma. Is that right?

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

Posted by: Mike Stay on February 23, 2008 11:04 PM | Permalink | Reply to this

Re: Logicians Needed Now

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?

Posted by: John Armstrong on February 24, 2008 1:02 AM | Permalink | Reply to this

Re: Logicians Needed Now

OK, I can see how syntactic subtleties can differentiate these. In lambda calculus, the term

(1)(square(x,y,z)square(x)+square(y)+square(z))(xx*x) (square \mapsto (x, y, z) \mapsto square(x) + square(y) + square(z))(x \mapsto x*x)

is the same morphism (via beta reduction) as

(2)(x,y,z)x*x+y*y+z*z. (x, y, z) \mapsto x*x + y*y + z*z.

The cut rule, on the other hand, talks about taking a pair of morphisms

(3)(square(x,y,z)square(x)+square(y)+square(z),xx*x) (square \mapsto (x, y, z) \mapsto square(x) + square(y) + square(z), x \mapsto x*x)

and spitting out the morphism above.

Posted by: Mike Stay on February 25, 2008 12:46 AM | Permalink | Reply to this

Re: Logicians Needed Now

Yes! And I’m very glad you mentioned beta reduction, because that is a key for one way of thinking about cut elimination. (I wish I had thought to say this earlier, because not long ago there was this course on classical and quantum computation, when you guys were discussing things like lambda calculus and beta reduction.)

As I’m sure you know, there is this so-called “Curry-Howard” correspondence, by which one can inter-translate between formulas and types, and between proofs and programs (or lambda terms). I’m going to put it a bit roughly, but it can all be made quite precise.

The way I think of it is: a deduction ff of a sequent

A 1,,A nBA_1, \ldots, A_n \vdash B

corresponds to a term f(a 1,,a n)f(a_1, \ldots, a_n) of type BB, where each a ia_i is a term of type A iA_i which occurs freely. Then, for example, one can interpret a deduction ending with the rule

Γ,AfBΓAB\frac{\Gamma, A \stackrel{f}{\vdash} B}{\Gamma \vdash A \multimap B}

in lambda terms as an instance of lambda abstraction, which binds a hitherto free variable aa of type AA: the term for this deduction would look like

λa.f(x 1,,x m,a)\lambda a. f(x_1, \ldots, x_m, a)

where now the free variables are those of the types X 1X_1, …, X mX_m appearing in Γ\Gamma.

Well, this much may have been obvious already, so let’s continue. Consider then a sequent deduction which introduces \multimap on the left of the turnstyle:

Δ,BgC;ΩαAΔ,AB,ΩC\frac{\Delta, B \stackrel{g}{\vdash} C; \Omega \stackrel{\alpha}{\vdash} A}{\Delta, A \multimap B, \Omega \vdash C}

Here, to get the corresponding lambda term, we need a fresh variable ϕ\phi of function space type ABA \multimap B. It occurs freely in the term

g(y 1,,y n,ϕ(α(z 1,,z p)))g(y_1, \ldots, y_n, \phi(\alpha(z_1, \ldots, z_p)))

[where the y iy_i are variables of types occurring in Δ\Delta, and the z jz_j are of types occurring in Ω\Omega]. This is the term associated with the previous deduction.

Now suppose we try to “cut” the previous two deductions at the formula ABA \multimap B. This corresponds to substituting the term

[λa.f(x 1,,x m,a)][\lambda a. f(x_1, \ldots, x_m, a)]

(of type ABA \multimap B) in for the free variable ϕ\phi. (I guess this is the “function call”.) But the computation then involves evaluating the expression

[λa.f(x 1,,x m,a)](α(z 1,,z p))[\lambda a. f(x_1, \ldots, x_m, a)](\alpha(z_1, \ldots, z_p))

which is where we use beta reduction; it reduces to

f(x 1,,x m,α(z 1,,z p)).f(x_1, \ldots, x_m, \alpha(z_1, \ldots, z_p)).

What this reduction has done is “push back” [or inline?] a substitution of a term for a variable ϕ\phi of type ABA \multimap B, in favor of substitutions of terms of simpler type. One is the substitution of α(z 1,,z p)\alpha(z_1, \ldots, z_p) for the variable aa of type AA. The other substitutes the term in the last display (a term of type BB) for the variable bb in g(y 1,,y n,b)g(y_1, \ldots, y_n, b).

At the level of sequent deductions, this inlining step pushes back the cuts [where we make the substitutions], from the cut at the formula ABA \multimap B, to cuts at the simpler formulas AA and BB. In fact, this is exactly the case 6 of the cut elimination algorithm that I was trying to point you to in the comment below, on page 106 of Proofs and Types. This is the case which corresponds precisely to beta reduction.

Posted by: Todd Trimble on February 25, 2008 3:29 AM | Permalink | Reply to this

Re: Logicians Needed Now

It’s \multimap.

Thank you!

I’m trying to understand: we’ve got a symmetric monoidal closed category AA, and we “interpret it in BB” by taking a symmetric monoidal functor F:ABF: A \to B. Then we use the fact that BB is equivalent to its skeleton CC; calling that equivalence E, we get EF:ACE F: A \to C. Then we pull the monoidal structure on CC back to AA 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,]F[X, Y, Z, \ldots] (generated by a set or discrete category of positive literals XX, YY, ZZ, …). The objects of the free structure are MILL formulas, and the morphisms ABA \to B are equivalence classes of MILL-valid deductions of sequents ABA \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,,A nBA_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]F[X, Y, Z] (as a monoidal category). For details on this underlying multicategory construction, see Tom Leinster’s book, page 84 (his V 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 MM to get a strict monoidal category M M^\prime monoidally equivalent to MM. 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 M^\prime are finite lists of objects of MM. Then, to each finite list Γ=A 1,,A n\Gamma = A_1, \ldots, A_n one can associate a “clique” which is the diagram of all ways of tensoring up the A iA_i in order, possibly with copies of II thrown in, and isomorphisms between them based on the monoidal structure in MM. (One thinks of each nn-fold tensoring as tagged by a planar tree τ\tau with nn 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 τ,τ : τΓ τ Γf_{\tau, \tau^\prime}: \otimes_\tau \Gamma \to \otimes_{\tau^\prime} \Gamma between the two tensorings in MM.)

Then, a morphism ΓΔ\Gamma \to \Delta in the strictification M M^\prime is just the obvious notion of clique morphism: a collection of maps in MM 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 τ,τ f_{\tau, \tau^\prime}, f σ,σ f_{\sigma, \sigma^\prime} in the sense of making all the triangles commute. For example, f τ,τ 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 M^\prime becomes strict monoidal; on objects the tensor product is concatenation of lists. MM is embedded inside M 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 MM, namely to any of its tensorings τΓ\otimes_\tau \Gamma). So, that’s the formal strictification.

Hence, (equivalence classes of) deductions of sequents ΓA\Gamma \vdash A can be interpreted as morphisms ΓA\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 ABA \vdash B and BCB \vdash C, then anywhere in a proof of ACA \vdash C mentioning BB you can inline the proof of BB 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 CDC \Rightarrow D. (Girard et al. are dealing with classical = non-intuitionistic sequents; to remove clutter and put yourself in MILL, take B̲\underline{B} and B ̲\underline{B^\prime} to be empty, and B ̲\underline{B^{\prime\prime}} to be a singleton.) Here the deduction (which ends with cutting at CDC \Rightarrow D) is replaced by a deduction involving two cuts, one at CC and one at DD. 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 XXX \vdash X on literals XX), 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.

Posted by: Todd Trimble on February 24, 2008 2:46 AM | Permalink | Reply to this

Re: Logicians Needed Now

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,]F[X,Y,Z,\ldots] (generated by a set or discrete category of positive literals X,Y,Z,X, Y, Z, \ldots). The objects of the free structure are MILL formulas, and the morphisms ABA\to B are equivalence classes of MILL-valid deductions of sequents AB.A\vdash B.

OK, at first glance I thought this was different from what we’re doing, but I think I understand: our objects are generated by the literals and the two connectives \otimes and ,\multimap, and we consider ABA \vdash B to be the set of morphisms hom(A,B).hom(A, B). Then inference rules are dinatural transformations between special functors from

(1)C n×(C op) mSet.C^n \times (C^{op})^m \to Set.

The coherence laws on the natural transformations assert that two different deductions (two ways of going around the diagram) are “equal.”

Your objects are the functors (lines in a deduction) and your morphisms are the dinatural transformations (coherence-law-equivalence classes of deductions).

Ah! Yes, you say so:

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).

John Baez wrote:

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

(2)(X 1,,X n)(Y 1,,Y m)=(X 1,,X n,Y 1,,Y m) (X_1,\ldots,X_n)\otimes (Y_1,\ldots,Y_m)=(X_1,\ldots,X_n,Y_1,\ldots,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 how does the subformula property play into all this?

Posted by: Mike Stay on February 25, 2008 12:36 AM | Permalink | Reply to this

Re: Logicians Needed Now

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 AA, and we “interpret it in BB” by taking a symmetric monoidal functor F:AB.F:A\to B. Then we use the fact that BB is equivalent to its skeleton CC; calling that equivalence E,E, we get EF:AC.E F:A \to C. Then we pull the monoidal structure on CC back to AA 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:XY)ZX(YZ)a_{X,Y,Z} : X \otimes Y) \otimes Z \stackrel{\sim}{\to} X \otimes (Y \otimes Z)

Switching to a skeletal subcategory ensures that

(XY)Z=X(YZ)(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,,X n)(Y 1,,Y m)=(X 1,,X n,Y 1,,Y m)(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!

Posted by: John Baez on February 24, 2008 4:48 AM | Permalink | Reply to this

Re: Logicians Needed Now

Yes, that’s the mistake I was making. Thanks!

Posted by: Mike Stay on February 24, 2008 9:44 PM | Permalink | Reply to this

Re: Logicians Needed Now

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.

Posted by: Robin on February 24, 2008 9:37 AM | Permalink | Reply to this

Re: Logicians Needed Now

Todd wrote:

But it should come as no surprise that to get away with a cut elimination theorem, one has to be very careful in just how the deductive system is set up — sometimes a delicate matter.

I can believe that. But, to the extent to which the consequences of cut elimination can be phrased as theorems about symmetric monoidal closed categories, I’d naively hope we could phrase these consequences in a way that doesn’t give a darn whether we’re talking about a symmetric monoidal closed category or its strictification. After all, they’re equivalent!

I’m not denying that to prove cut elimination, this strictification business could be crucial — but that’s a matter of ‘technique’ rather than ‘results’. (There’s some rule of thumb in category theory saying that your theorems should be stated in a way that’s invariant under equivalence, but you’re allowed to use tricks like skeletons or strictifications to prove these theorems.)

If my hope is true, I could protect my delicate physicist readers from those scary ‘sequents’

A 1,,A nBA_1, \dots, A_n \vdash B

and just stick to the formalism where we write

A 1A nBA_1 \otimes \cdots \otimes A_n \vdash B

as faux-logician’s notation for the homset

hom(A 1A n,B)hom(A_1 \otimes \cdots \otimes A_n, B)

You seem to be confirming my hopes here:

There is also a more refined, categorified cut elimination, which allows one to decide not only if there exists a morphism ABA \to B, but whether two such morphisms built from syntactically different deductions are the same on the basis of the axioms (commutative diagrams) for the type of structured monoidal category being studied. This is the crucial step toward solving a coherence problem for that type of structure, i.e., deciding which diagrams commute. The fact that Gentzen cut elimination admits a categorified form is one of the great insights due to Lambek.

It sounds, ironically, that this ‘more refined’ cut elimination theorem may take less work to explain — the result, that is, not the proof.

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?

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?

This is probably all in your thesis. I want it! I hope you send it to me and let me scan it in and put it on my website.

Posted by: John Baez on February 24, 2008 9:26 PM | Permalink | Reply to this

Re: Logicians Needed Now

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 CC are equal, then there’s a procedure for deciding equality in F[C]F[C] relative to equality in CC.

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]F[C] is equivalent to a kind of “wreath product” F[1]CF[1] \int C. So really, “all” you need to know is the structure of F[1]F[1] (where 11 is the 1-object 1-morphism category); then, with the help of your CC-oracle, you know all about F[C]F[C]. The same type of thing holds whenever the theory or doctrine is expressible as a so-called “club”.

Posted by: Todd Trimble on February 24, 2008 11:01 PM | Permalink | Reply to this

Re: Logicians Needed Now

John,

This looks like a very interesting paper!

I haven’t reached the logic part yet, but I’m not at all sure that your Definition 15 (defining a compact monoidal category) is equivalent to the usual definition.

Rather trivially, does it even follow from your definition that * is an equivalence? Less trivially, even if it does (or if you add that as an extra condition), I don’t know how to show that the zig-zag conditions hold. Do you have an argument that they do?

(I think I raised this here once before, with Todd.)

Posted by: Robin on February 21, 2008 4:14 PM | Permalink | Reply to this

Re: Logicians Needed Now

The definition you mention is our definition of a ‘compact monoidal category’, not necessarily symmetric or even braided. It seems most people don’t use the term ‘compact’ until the category is at least braided. What we’re calling a ‘compact monoidal category’ is supposed to match what some people call an autonomous category, or more precisely a ‘right autonomous category’: a monoidal category where every object has a right dual. But, let me continue to use the term ‘compact monoidal category’ here.

Please tell me if the following seems correct, or if you want more details on some point, or if something seems wrong!

In a monoidal category CC where every object has a right dual, we can randomly pick a right dual X *X^* for every object XX. This choice then extends uniquely to a contravariant functor * R:CC*_R : C \to C.

There is, however, no obvious reason why this functor need be an equivalence unless every object also has a left dual! In that case, we also get a contravariant functor * L:CC*_L : C \to C, and both * L* R*_L *_R and * R* L*_R *_L are naturally isomorphic to the identity.

If CC is braided, every right dual automatically becomes a left dual, so * R*_R is automatically an equivalence in a braided monoidal category with right duals.

In our paper we take a slightly different tack, defining a (right) compact monoidal category to be a (right) closed monoidal category CC equipped with a contravariant functor *:CC* : C \to C such that the internal hom is (naturally isomorphic to) X *YX^* \otimes Y.

Given this, you should want to see how we get the unit and counit and zig-zag identities that make X *X^* into a right dual for XX. By the above remarks, you should not expect *:CC* : C \to C to be an equivalence. But, it will be automatically as soon as CC is braided — or more generally, as soon as CC is also left compact.

We describe how to get the unit i:1X *Xi: 1 \to X^* \otimes X and counit e:XX *1e: X \otimes X^* \to 1. (Note our conventions, which are backwards compared to those I normally use.) We do not describe how to get the zig-zag identities for ii and ee. But, these should follow from the fact that the functor X *X^* \otimes - is right adjoint to XX \otimes -. The unit and counit of adjoint functors always satisfy certain zig-zag identities, and these should imply the zig-zag identities for ii and ee. But now you’ve got me worried. You are, after all, the prince of compact closed categories!

Posted by: John Baez on February 23, 2008 4:06 AM | Permalink | Reply to this

Re: Logicians Needed Now

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 ϕ A,B,C:(AB,C)(B,A*C)\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:ABCf: A\otimes B\to C and object XX, we have ϕ(fX)=ϕ(f)X\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!

Posted by: Robin on February 23, 2008 11:30 AM | Permalink | Reply to this

Re: Logicians Needed Now

I’d actually like to come back to this issue, because I think I have an abstract argument that the Baez-Stay definition is alright after all at least in the symmetric case, but it should first be run past Robin’s eagle eye, and perhaps also shaken down to a simpler proof.

The argument goes like this: it suffices to show that the counit of the adjunction (X)(X *)(X \otimes -) \dashv (X^* \otimes -), call it ϵ\epsilon, is given componentwise by the composite

XX *YϵIYIYYX \otimes X^* \otimes Y \stackrel{\epsilon I \otimes Y}{\to} I \otimes Y \stackrel{\sim}{\to} Y

(and similarly for the unit), i.e., that the counit and unit are given by what they do at II.

Now, in the Stay-Baez definition, the counit ϵ\epsilon is given by transporting the structure of the counit of the adjunction (X)(X)(X \otimes -) \dashv (X \multimap -) across the isomorphism (X *)(X)(X^* \otimes -) \cong (X \multimap). This counit is just the evaluation map

X(XY)YX \otimes (X \multimap Y) \to Y

in the symmetric monoidal closed category, call it VV. Now this map, like every definable map in the theory of smc categories, is certainly VV-natural in the sense of enriched category theory. It follows by transport of structure that ϵ\epsilon carries VV-natural structure.

We get from the enriched transformation

ϵ:XX *YY\epsilon: X \otimes X^* \otimes Y \to Y

a transformation

XX *YYX \otimes X^* \to Y \multimap Y

which is VV-dinatural in YY. Hence this map factors uniquely through the VV-enriched end (if it exists). But

yyyI\int_y y \multimap y \cong I

by the enriched Yoneda lemma (which holds true in any smc). Tracing through that, we find the factorization is the obvious composite

XX *ϵIIyyX \otimes X^* \stackrel{\epsilon I}{\to} I \to y \multimap y

and this proves the desired claim.

Possibly I’ve overlooked some subtlety, but so far I’m not seeing anything wrong with this argument (although it may be needlessly fancy).

Posted by: Todd Trimble on February 25, 2008 6:05 PM | Permalink | Reply to this

Re: Logicians Needed Now

Todd,

This is awesome! I’ve suspected for ages that this might be true, but I wasn’t clever enough to think of this way of looking at it.

If I’m understanding aright, you almost got this last time we talked about it. You pointed out that the extra condition on the adjunction can be expressed as “a compatibility between the unit and counit … and the canonical strengths of these functors”; but it apparently didn’t occur to either of us, at the time, that this compatibility is already a standard fact about closed categories!

I’m going to work through this some more now, to make sure I understand it properly, but it looks wonderful so far.

Robin

Posted by: Robin on February 26, 2008 12:39 PM | Permalink | Reply to this

Re: Logicians Needed Now

Just to put a little gloss on it: it’s not just that we have e.g., a counit of (X)(X *)(X \otimes -) \dashv (X^* \otimes -):

XX *YY;X \otimes X^* \otimes Y \to Y;

we also have the adjunction (Y)(Y *)(- \otimes Y) \dashv (- \otimes Y^*) which allows us to “decouple” XX and YY (whereupon we can apply the Yoneda reduction trick, or some other device). I think maybe the two of us might have been getting hung up on just the (X)(X *)(X \otimes -) \dashv (X^* \otimes -) part (speak for myself).

Symmetry comes into play for the adjunction (Y)(Y *)(- \otimes Y) \dashv (- \otimes Y^*). So all bets are off (for me) whether the Baez-Stay definition holds up for the closed monoidal case, although I’m pretty sure that it all works out fine for the braided monoidal case (which John and Mike apparently want).

Posted by: Todd Trimble on February 26, 2008 3:26 PM | Permalink | Reply to this

Re: Logicians Needed Now

Actually, it’s become clear to me that I don’t yet understand your argument. The argument sketched in my comment above, which I incorrectly thought was equivalent to yours, appears to be circular.

What I mean is this: in any smcc, the functor BB \multimap - for a fixed object BB carries a canonical strength. Also the functor B *-\otimes B^* carries a canonical strength for any object B *B^*. But even if these two functors are isomorphic, their strengths are not obviously generally the same; in fact the claim that they are the same turns out to be equivalent to the original question, whence the circularity.

Now I need to think about your actual argument, and convince myself that the circularity does not arise there!

Posted by: Robin on February 26, 2008 4:20 PM | Permalink | Reply to this

Re: Logicians Needed Now

Okay, I think I must be missing something here.

We have a strong (i.e. enriched) transformation

(1)ϵ:X(XY)Y\epsilon: X\otimes(X\multimap Y) \to Y

But this is strong in YY with respect to the canonical strength of the functor XX\multimap-, whereas it looks as though you need it to be strong with respect to the canonical strength of X *X^*\otimes-.

Can Todd or anyone help me?

Posted by: Robin on February 26, 2008 4:47 PM | Permalink | Reply to this

Re: Logicians Needed Now

Let me see if this helps. I agree that the two strengths are not a priori the same. I am going to use the strength on X *X^* \otimes - where we think of it as XX \multimap -.

Then the evaluation map

XX *YYX \otimes X^* \otimes Y \to Y

is VV-natural in YY. But by the VV-adjunction (Y)(Y)(- \otimes Y) \dashv (Y \multimap -), we transform this to

XX *YYX \otimes X^* \to Y \multimap Y

which is VV-dinatural in YY. Then apply the Yoneda reduction trick.

Although I continue to see nothing illegal about any of this, I still want to filter this through your brain. It is, admittedly, a somewhat tricky argument.

Posted by: Todd Trimble on February 26, 2008 5:02 PM | Permalink | Reply to this

Re: Logicians Needed Now

Just to be clear, I am not claiming that there is anything wrong here. I’m just struggling to understand what you’re doing, presumably by missing something obvious.

What continues to puzzle me is this: we have a strong adjunction

(1)(Y)(Y)(-\otimes Y) \dashv (Y\multimap -)

where, implicitly, the functor on the left has the strength associated with tensor. We have a strong natural transformation

(2)(XX *)()(X\otimes X^*\otimes -) \to (-)

where the functor on the left has the strength associated with the internal hom.

You agree that these strengths are a priori different. So there seem to be two different strong functors here (i.e. two different strengths for the same functor). The strong functor in the adjunction is not the same as the strong functor in the natural transformation. So how can you (strongly) apply the one to the other?

Posted by: Robin on February 26, 2008 5:59 PM | Permalink | Reply to this

Re: Logicians Needed Now

where the functor on the left has the strength associated with the internal hom.

Right, the functor X *X^* \otimes - is given the strength of the internal hom.

two different strengths for the same functor

Not the same functor! One is X *X^* \otimes -, the other is Y- \otimes Y.

Well, I’m starting to get a little nervous now, but I don’t think I’m quite dead yet. We have a transformation of the form

AYYA \otimes Y \to Y

which is VV-natural in YY, where I have used AA as an abbreviation for XX *X \otimes X^*. Hit both sides with ZZ \multimap - (where I’m going to instantiate ZZ at YY in a moment). Then we get

Z(AY)ZYZ \multimap (A \otimes Y) \to Z \multimap Y

which is VV-natural in YY, ZZ. Now instantiate ZZ at YY and precompose with the component of the unit of (Y)(Y)(- \otimes Y) \dashv (Y \multimap -) at AA:

AY(AY).A \to Y \multimap (A \otimes Y).

The VV-dinaturality in YY of that unit component at AA is clear, and has nothing to do with the internal enriched structure we happened to use for AA \otimes -. Now compose these two VV-extranatural transformations to get

AYYA \to Y \multimap Y

which is VV-dinatural in YY.

Or do you see something wrong with this?

Posted by: Todd Trimble on February 26, 2008 6:47 PM | Permalink | Reply to this

Re: Logicians Needed Now

I’m not sure how long I should continue to publicly humiliate myself here. I’m tempted to move the conversation to email, but perhaps there is something to be gained by letting the air in.

I’m about 95% sure you’re right, but I still don’t understand why. Fortunately you’ve been kind enough to lay out the procedure step-by-step, so I think I can pinpoint the part that’s confusing me.

It’s when you say

The V-dinaturality in Y of that unit component at A is clear, and has nothing to do with the internal enriched structure we happened to use for AA\otimes−.

Sorry to be so dense, but I don’t get that. I know why it’s VV-dinatural in YY when you take the usual VV-functor AA\otimes−, but I don’t understand why that should continue to be the case for some other VV-functor “AA\otimes−”, even if it has the same underlying ordinary functor.

Posted by: Robin on February 26, 2008 10:16 PM | Permalink | Reply to this

Re: Logicians Needed Now

Robin, you’re not humiliating yourself – I’m afraid the honor of that will probably go to me! :-/

Yesterday afternoon I drove in to NYC, and at length during the car ride it gradually dawned on me that I would probably have a hard time proving the unit was dinatural in YY unless I assumed that this functor in two variables AA and YY was indeed the standard tensor AYA \otimes Y (with its standard strength). Bah!

So I’m probably going to have to retract the claim (and I appreciate your dragging it out of me; my mistake might well have gone undetected were it not for your persistence in checking the details).

This is the damnedest problem! Now we’re going to have to get this resolved one way or the other.

Posted by: Todd Trimble on February 27, 2008 5:11 PM | Permalink | Reply to this

Re: Logicians Needed Now

Although it’s reassuring to hear that I wasn’t being as stupid as I feared, it’s disappointing that we have yet to get to the bottom of this!

For the benefit of anyone else who is playing (if anyone is), I did find a partial solution last time Todd and I discussed this:

If the tensor unit II is a generator (equivalently a cogenerator) then the Baez-Stay definition does imply compact closure.

Unfortunately there do seem to be (rare) cases of compact closed categories in which II is not a generator, so this doesn’t solve the full problem, but perhaps it goes some way to explaining the apparent elusiveness of counterexamples.

One of the lesser-known characterisations of compact closure is this: a symmetric monoidal closed category is compact closed iff the canonical natural transformation

(1)(AI)BAB(A\multimap I)\otimes B \to A \multimap B

is invertible. The Baez-Stay definition (in the symmetric case) is equivalent to “a symmetric monoidal closed category such that (AI)B(A\multimap I)\otimes B is naturally isomorphic to ABA\multimap B”. So, we can reformulate the question as follows: if (AI)B(A\multimap I)\otimes B is naturally isomorphic to ABA\multimap B, then is it necessarily the case that the canonical natural transformation (AI)BAB(A\multimap I)\otimes B \to A\multimap B is invertible?

There are some theorems to the effect that, if two things are isomorphic, then the canonical map from one to the other must be invertible. So it’s not a totally ridiculous thing to wonder about. But of course there are plenty of other cases where this is not true, and I suspect the present case may be one such.

So I’m currently leaning towards the possibility of a counterexample, but I haven’t found one yet!

Posted by: Robin on February 28, 2008 2:08 PM | Permalink | Reply to this

Re: Logicians Needed Now

I imagine that at least John and Mike have been paying attention to this discussion.

One of the lesser-known characterisations of compact closure is this: a symmetric monoidal closed category is compact closed iff the canonical natural transformation (AI)BAB(A \multimap I) \otimes B \to A \multimap B is invertible.

Yes. I’d think it’s probably the best way to address the problem at this point (with deadlines looming), and fits well with a general philosophy that instead of just saying that two functors are isomorphic, one should specify the isomorphism whenever possible.

Posted by: Todd Trimble on February 28, 2008 2:42 PM | Permalink | Reply to this

Re: Logicians Needed Now

I had made a similar claim once here at the Café [that (X)(X *)(X \otimes -) \dashv (X^* \otimes -) implies compact closure], whereupon Robin contacted me privately and convinced me it ain’t necessarily so! Robin should be the one to explain, but the reason is somewhat subtle, and it’s a very easy mistake to make.

Posted by: Todd Trimble on February 23, 2008 5:11 AM | Permalink | Reply to this

Re: Logicians Needed Now

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)(X *)(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)(X *)(X \otimes −) \dashv (X^* \otimes −) for all XX implies compact closure” — surely this is true! Just take the unit and counit of the adjunction at stage II, which witness the fact that XX is left-dual to X *X^*.

From these morphisms we can construct an adjunction (X)(X *)(X \otimes − ) \dashv (X^* \otimes −), and I thought that the long discussion above was about whether every adjunction (X)(X *)(X \otimes − ) \dashv (X^* \otimes −) is of this form, with unit and counit deriving from the unit and counit at stage II. (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 XX has a right dual.

Posted by: Jamie Vicary on August 2, 2008 3:30 PM | Permalink | Reply to this

Re: Logicians Needed Now

Yes, this stuff is quite maddening. I could hardly believe it when Robin first brought it up, but as Robin is characteristically very careful, I knew it had to be looked into. And I still don’t see a way around his objection.

I know you know this, but let me review anyway. By definition, when we say that X * X^* is right dual to XX, we mean there are morphisms

η:IX *X \eta: I \to X^* \otimes X

ε:XX *I \varepsilon: X \otimes X^* \to I

such that the triangular equations hold:

1 X=(X1 XηXX *Xε1 XX) 1_X = (X \stackrel{1_X \otimes \eta}{\to} X \otimes X^* \otimes X \stackrel{\varepsilon \otimes 1_X}{\to} X)

1 X =(X η1 X X XX 1 X εX *) 1_{X^*} = (X^* \stackrel{\eta \otimes 1_{X^*}}{\to} X^* \otimes X \otimes X^* \stackrel{1_{X^*} \otimes \varepsilon}{\to} X^*)

where we assume we are working in a strict monoidal category to make things easier to state. Okay, as you point out, there’s not much choice as to what η\eta and ε\varepsilon should be: just put

η=u I:IX *X \eta = u_I: I \to X^* \otimes X

ε=c I:XX *I \varepsilon = c_I: X \otimes X^* \to I

where uu denotes the unit and cc the counit of the adjunction (X)(X *) (X \otimes -) \dashv (X^* \otimes -) we are given.

Now: how do you show the triangular equations above hold? Note that the triangular equations for (X)(X *)(X \otimes -) \dashv (X^* \otimes -) give e.g. that

1 X=(XXu IXX *Xc XIX) 1_X = (X \stackrel{X \otimes u_I}{\to} X \otimes X^* \otimes X \stackrel{c_{X \otimes I}}{\to} X)

but as far as either Robin or I can tell, this doesn’t give the actual triangular equation we want (which we would have of course if c XI=c I1 Xc_{X \otimes I} = c_I \otimes 1_X, but that was the point under debate).

It would be great to put this issue to bed once and for all, because neither of us cooked up an example where compact closure didn’t hold in this situation. And it was driving us nuts (or me, anyway).

Posted by: Todd Trimble on August 2, 2008 10:39 PM | Permalink | Reply to this

Re: Logicians Needed Now

I can confirm that it was driving me nuts too. It still does, when I think about it.

Counterexamples for this sort of thing seem remarkably difficult to cook up. I did come up with a messy, convoluted thing that looked as though it ought to be a counterexample, but I couldn’t see how to prove that it really was.

Posted by: Robin Houston on August 3, 2008 9:56 AM | Permalink | Reply to this

Re: Logicians Needed Now

Blast… thanks for those comments, Todd and Robin.

Robin pointed out earlier that everything’s OK in a category where II is generating, but there’s a good source of otherwise well-behaved categories where this isn’t true: monoidal semisimple categories, for which every object is isomorphic to a direct sum of a unique finite list of simple objects, up to permutation. We pick a field, kk, and choose the morphisms between two simple objects to be the elements of kk if the objects are isomorphic, but just the zero morphism if they’re not.

For kk the complex numbers, the compact closed such categories are exactly the representation categories of compact groups. Avoiding these, it’s easy to come up with loads of non-compact closed monoidal categories for which II isn’t generating.

Posted by: Jamie Vicary on August 3, 2008 12:33 PM | Permalink | Reply to this

Re: Logicians Needed Now

Dear Todd, Robin and John:

Boy am I glad I discovered this discussion. There was a big Paradox in some work I have been doing, and for the life of me I couldn’t ‘triangulate’ the problem. Then I met Jamie at the Categories, Logic and Foundations of Physics workshop in Oxford this weekend, and he told me about this discussion here at the n-café. Sure enough, it was the source of my anguish.

The extra condition required, besides VV \otimes - being left adjoint to V *V^* \otimes -, to make sure that V *V^* be a right dual of VV, is indeed just as Todd said above: at the level of units and counits we need

(1)c XI=c I1 X c_{X \otimes I} = c_I \otimes 1_X

Or, at the level of hom-set isomorphisms

(2)ϕ:Hom(XA,B)Hom(A,X *B) \phi : Hom(X \otimes A, B) \rightarrow Hom(A, X^* \otimes B)

(which was the context which started off this whole discussion, since John and Mike had originally formulated compact closure at this level in Definition 15 of the original draft), we need to have the extra condition:

(3)ϕ(fid)=ϕ(f)id. \phi(f \otimes id) = \phi(f) \otimes id.

You can see these conditions nicely in string diagrams of course :-)

As far as counterexamples go, I haven’t really thought about an explicit one but I can say this: the extra condition is indeed necessary, because without it, one can prove facts about fusion categories (semisimple rigid linear monoidal categories) which are definitely not true. That was the source of the Paradox I had been quagmired in.

Posted by: Bruce Bartlett on August 26, 2008 3:54 PM | Permalink | Reply to this

Re: Logicians Needed Now

Needless to say, I’d love to see your demonstration of why the extra condition is necessary!

Posted by: Robin Houston on August 26, 2008 8:24 PM | Permalink | Reply to this

Re: Logicians Needed Now

It’s great you’ve sorted your problem out! This blog is tremendously useful as a repository of discussions of fiddly problems.

As far as counterexamples go, I haven’t really thought about an explicit one but I can say this: the extra condition is indeed necessary, because without it, one can prove facts about fusion categories (semisimple rigid linear monoidal categories) which are definitely not true. That was the source of the Paradox I had been quagmired in.

But this is great — if you can prove absurd things, then surely that means you’re only inches away from a counterexample, which would make all this a lot clearer. What’s the simplest fusion category in which your paradox arises? And what is the paradox, anyway?

Posted by: Jamie Vicary on August 26, 2008 9:39 PM | Permalink | Reply to this

Re: Logicians Needed Now

Bruce wrote:

Boy am I glad I discovered this discussion. There was a big Paradox in some work I have been doing, and for the life of me I couldn’t ‘triangulate’ the problem.

This is a great example of how category theory connects different subjects. A discussion focused on logic turned out to be the key to saving you from a paradox in topological quantum field theory!

As far as counterexamples go, I haven’t really thought about an explicit one but I can say this: the extra condition is indeed necessary, because without it, one can prove facts about fusion categories (semisimple rigid linear monoidal categories) which are definitely not true.

That would settle Todd and Robin’s question, then.

By the way, Mike Stay and I are working on another draft of our Rosetta Stone paper, which should give a correct treatment of combinator calculi for symmetric monoidal categories. This was the biggest problem with the earlier draft.

Posted by: John Baez on August 26, 2008 7:34 PM | Permalink | Reply to this

Re: Logicians Needed Now

That would settle Todd and Robin’s question, then.

An explicit example would be very welcome. I might have another go at it myself, soon.

By the way, Mike Stay and I are working on another draft of our Rosetta Stone paper, which should give a correct treatment of combinator calculi for symmetric monoidal categories. This was the biggest problem with the earlier draft.

Looking forward to it!

Posted by: Todd Trimble on August 26, 2008 8:33 PM | Permalink | Reply to this

Re: Logicians Needed Now

Robin wrote a while ago:

I can confirm that it was driving me nuts too.

Ah I know the feeling! Okay, here’s an explicit counterexample, coming from the world of fusion categories. A fusion category is a semisimple \mathbb{C}-linear monoidal category where each object has a dual (semisimplicity implies this dual is necessarily two-sided). In the simplest case as Jamie said above, think: “something which looks like Rep(G)Rep(G) for GG a finite group”, though we do not assume braidings or anything like that.

To remind yourself about the basic facts of fusion categories, look at these notes of Michael Mueger or these slightly older notes by Calaque and Etingof, or the three lectures by Boyarchenko at the bottom of the Geometric Langlands page. I also have some simple notes here which I was working on a while ago and am now writing up for thesis purposes; I needed some results there for a recent paper I wrote.

The important thing to understand about fusion categories is that they are semisimple — so there are a bunch of simple objects X iX_i (where simple means End(X i)=End(X_i) = \mathbb{C}) and everything else is a direct sum of them. The key data is the fusion rules:

(1)X iX j kN ij kX k X_i \otimes X_j \cong \bigoplus_k N^k_{ij} X_k

(By the way, I prefer to write an equals sign above, since the direct sum symbol should always be understood as a categorical direct sum (biproduct). But when you do that, someone always (incorrectly) complains!)

Now for the counterexample. We are trying to show that having natural isomorphisms

(2)ϕ:Hom(XA,B)Hom(A,X *B) \phi: Hom(X \otimes A, B) \rightarrow Hom(A, X^* \otimes B)

is strictly weaker than setting X *X^* up as a right dual of XX. I will give you an explicit example.

Namely, start with a simple object X i *X_i^* which is a right dual of X iX_i. Then we can construct ‘bad’ natural isomorphisms

(3)ψ:Hom(X i *A,B)Hom(A,X iB) \psi : Hom(X_i^* \otimes A, B) \rightarrow Hom(A, X_i \otimes B)

which don’t equip X iX_i as a right dual of X i *X_i^* as follows. Basically, our category is semisimple so all the hom-sets are in duality; i.e. for any two objects AA and BB there is a canonical isomorphism

(4)s:Hom(A,B)Hom(B,A) s : Hom(A, B) \rightarrow Hom(B, A)^\vee

where Hom(B,A) Hom(B, A)^\vee is the dual vector space. (There is much more that can be said here, but I will stick to the simplest possible situation). Basically you expand a map f:ABf : A \rightarrow B in terms of a basis a i,p:X iAa_{i,p} : X_i \rightarrow A and b i,q:X iBb_{i,q} : X_i \rightarrow B coming from the simple objects, and take the “trace”.

This means we can define ψ\psi as the composite

(5)ψ:=Hom(X i *A,B)sHom(B,X i *A) ϕ Hom(X iB,A) s 1Hom(A,X iB). \psi := Hom(X_i^* \otimes A, B) \stackrel{s}{\rightarrow} Hom(B, X_i^* \otimes A)^\vee \stackrel{\phi^\vee}{\rightarrow} Hom(X_i \otimes B, A)^\vee \stackrel{s^{-1}}{\rightarrow} Hom(A, X_i \otimes B).

This principle of using the duality on the hom-sets to turn right adjoints into left adjoints will be familiar to algebraic geometers since it is really using the “trivial Serre functor” on a semisimple category. I needed to use it in the setting of 2-Hilbert spaces in this paper.

Now, from the big discussion above, we know that in order for ψ\psi to present X iX_i as a right dual of X i *X_i^*, it needs to satisfy

(6)ψ(fid)=ψ(f)id. \psi(f \otimes \id) = \psi(f) \otimes \id.

In the simplest situation when

(7)A=X j,f=id X i *,B=X i *X j A = X_j, f = id_{X_i^*}, B= X_i^* \otimes X_j

we find (after some calculation, best done in string diagrams!) that ψ(idid)=ψ(id)id\psi (id \otimes id) = \psi(id) \otimes id would imply that

(8)1= kN ij k 1 = \sum_k N_{ij}^k

which is clearly wrong! Thus ψ\psi does not give X iX_i the structure of a right dual of X i *X_i^*.

Another viewpoint on this thing, from the perspective of algebraic geometry, can be found in my supervisor Simon Willerton and Andrei Caldararu’s recent paper on the Mukai pairing via string diagrams. Basically this property of having ψ(fid)=ψ(f)id\psi(f \otimes id) = \psi(f) \otimes \id is precisely the property that

Taking partial traces must not affect the Serre trace.

This result proved to be key to their paper — it is Theorem 4! (See it there in string diagrams). So — something which was important in logic is not only important in TQFT, it’s also critical in algebraic geometry.

Posted by: Bruce Bartlett on August 26, 2008 10:45 PM | Permalink | Reply to this

Re: Logicians Needed Now

Well! We can all breathe a big sigh of relief now!

Thank you very much, Bruce, for taking the time to explain all this. Another problem put to bed, at long last.

Posted by: Todd Trimble on August 27, 2008 1:09 AM | Permalink | Reply to this

Re: Logicians Needed Now

Okay, I’ve read the logic part now!

Todd has already said most of what I thought. I’m not sure I can do much more than to repeat some of it in slightly different words.

The sequent calculus has the remarkable properties that it both enjoys the subformula property and admits cut. This combination is what makes it a powerful tool. For example: since every application of a rule (in the linear setting) adds a single connective, the number of steps in a proof is equal to the number of connectives in the conclusion. In particular each sequent admits at most a finite number of proofs. From this it follows, without much trouble, that in the free s.m.c.c. on a set of objects, each hom-set is finite. I don’t know any other way to prove that. As Todd says, this line of thinking can be pursued further to extract a concrete description of the arrows of a free s.m.c.c.

I’m sure that’s more than you want to get into in an overview paper like this; but (at least to me) the interesting thing about the sequent calculus is that it gives a surprising, alternative way to describe the morphisms of a s.m.c.c. Your formal system instead mirrors the usual categorical description, which makes it obvious that it’s equivalent to the categorical description (as was presumably your intent), but with some risk of making the exercise vacuous.

On the other hand I can understand that, to someone who’s never seen anything of the sort before, it would no doubt be surprising that the tensor and internal hom connectives can be interpreted as conjunction and implication in such a way that the categorical operations are truth-preserving, so I suppose it does make a useful pedagogical point after all!

Posted by: Robin on February 21, 2008 5:22 PM | Permalink | Reply to this

Re: Logicians Needed Now

Thanks for the comments, Todd and Robin. First quick comment. Robin writes:

…(at least to me) the interesting thing about the sequent calculus is that it gives a surprising, alternative way to describe the morphisms of a s.m.c.c.

Do you have a reference where someone actually does this — for a mere s.m.c.c.? All the references I’ve found seem to tackle more complicated systems, which are too rich for my blood. I would love to see a sequent calculus that precisely matched the theory of s.m.c.c’s. I would love to talk about that.

Gulp. Suddenly, with a sinking feeling, I seem to recall that it was Todd who did this! If so, how could I have forgotten??? Is it true?

Posted by: John Baez on February 21, 2008 5:53 PM | Permalink | Reply to this

Re: Logicians Needed Now

The history actually goes back a ways.

The earliest printed reference that I know of, for the sequent calculus pertaining to symmetric monoidal closed categories, is

  • Manfred Szabo, Algebra of Proofs. Studies in Logic and the Foundations of Mathematics, vol. 88, North-Holland (1978).

In this book, Szabo presents a whole batch of sequent calculi for structured categories: for monoidal, symmetric monoidal, symmetric monoidal closed, cartesian closed, …, even toposes. He also gives cut elimination algorithms for each of these cases.

Sadly, there’s a bit of controversy about this book: Szabo attempted to go further, to give normalization algorithms for deciding coherence problems in each of these cases. But they falter for at least all the cases which involve a symmetry isomorphism. The coherence problem for symmetric monoidal closed categories was a notoriously thorny problem which was the subject of not a few papers and Ph.D. dissertations, including my own.

But aside from that, this book holds a place in my heart because it’s where I first learned the details behind sequent calculus, and for the purposes of learning that alone, I don’t think the book can be much faulted. I can vouch for the accuracy of the presentation of sequent calculus for smc categories.

It was Richard Blute in his dissertation who established the connections between linear logic and coherence problems for structures with a linear logic flavor (including smc categories). My dissertation came out a little while later (where I gave a full solution of the coherence problem for smc categories), and was never published. In other words, don’t feel a bit bad that you didn’t remember that, John.

Posted by: Todd Trimble on February 21, 2008 10:01 PM | Permalink | Reply to this

Re: Logicians Needed Now

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?

Posted by: Robin on February 21, 2008 10:10 PM | Permalink | Reply to this

Re: Logicians Needed Now

I believe Rick’s thesis was published; I can’t be absolutely sure of the title, but I have a feeling it may be

  • Linear logic, coherence, and dinaturality, Theor. Comp. Sci. 115 (1), 1993.

A closer look at Google seems to confirm that suspicion.

Posted by: Todd Trimble on February 21, 2008 10:19 PM | Permalink | Reply to this

Re: Logicians Needed Now

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

Posted by: Tom Leinster on February 21, 2008 10:41 PM | Permalink | Reply to this

Re: Logicians Needed Now

I’ll consider doing that. As next best thing, I’ll direct attention to

where some of the methods developed in my thesis played a significant role in treating “the problem of the unit” (see material on “thinning links” and the “rewiring theorems”).

Posted by: Todd Trimble on February 22, 2008 1:17 AM | Permalink | Reply to this

Re: Logicians Needed Now

That’s an excellent question, John. I’m sorry not to have an equally good answer. As you suggest, I think it must be in Todd’s PhD thesis, which sadly is not easily available: I haven’t actually seen it myself.

My (now former) supervisor Andrea Schalk has some notes that contain (at the top of the second page) a sequent system that corresponds to SMCCs. Looking at it now, there is a rule missing: there ought to be a left-rule for the unit in addition to the right-rule that is there, viz:

ΓAΓ,IA\frac{\Gamma\vdash A}{\Gamma,I\vdash A}

It is fairly obvious that every proof can be interpreted in a closed, representable, symmetric multicategory. Since any such multicategory is equivalent, in a reasonable sense, to the SMCC obtained by restricting to the ordinary arrows, it follows that a proof of a simple sequent can be interpreted in any SMCC. (Say a sequent is simple if it has one formula on the left: that is probably not standard terminology.)

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.

There may well be somewhere that all this is beautifully explained. If so, I apologise to the author for not knowing about it or for having forgotten it. If not, it’s yet another of those things that is well-known to those who know it well. :-/

Incidentally, there’s a reasonably detailed explanation of cut-elimination in Proofs and Types, chapter 13.

Posted by: Robin on February 21, 2008 10:01 PM | Permalink | Reply to this

Re: Logicians Needed Now

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.

Posted by: Todd Trimble on February 22, 2008 12:09 AM | Permalink | Reply to this

Re: Logicians Needed Now

Do you have a precise statement of what it means to solve a coherence problem?

What I mean is: of course your characterisation is better than Szabo’s, but is there a generally-accepted precise sense in which yours is a solution and his isn’t? From what you’ve told us, Szabo didn’t actually have a way to choose a canonical proof from each equivalence class, though he thought he did. But one could always naively take the whole equivalence class as representative of a morphism. (Unless I’m very confused, these classes are finite, so they’re concrete things in the sense that they can be written down.)

Is it a question of computational complexity, i.e. that your approach gives an algorithm for deciding proof-equivalence in polynomial time, whereas Szabo’s doesn’t?

Posted by: Robin on February 22, 2008 1:17 PM | Permalink | Reply to this

Re: Logicians Needed Now

Excellent questions, Robin. (Just in case anyone has a hard time believing that Robin could extract information about my solution from the discussion above, I should say that the two of us had exchanged some emails on the topic some months back, where I outlined the main results.)

There is a sense in which the Lambek-equivalence classes (of cut-free proofs) are still infinite, because of the presence of the exchange rule

Γ,A,B,ΔCΓ,B,A,ΔC\frac{\Gamma, A, B, \Delta \to C}{\Gamma, B, A, \Delta \to C}

The commuting conversions which would control multiple applications of exchange would boil down to the relations in the standard presentation of the symmetric groups. Although the symmetric groups are bounded in size, the words in their generators are obviously not, hence the equivalence classes are infinite. And as I said, Szabo didn’t find a satisfactory way of dealing with symmetry.

It’s possible that this difficulty is completely spurious (that is, maybe there’s a simple way to address it), and I confess that I didn’t actually work through Barry Jay’s demonstration that Szabo’s solution doesn’t work. Modulo that particular snag, you’re right that in the event that one pares down to finite equivalence classes, that would have to be reckoned a solution in the mathematical sense, although (due in large part to the cumbersome nature of sequent proofs) hardly a satisfactory one on a human level, as you acknowledge.

Since you seem to be interested: the solution that Blute, Cockett, Seely, and Trimble gave to the coherence problem for *-autonomous categories is of the flavor you describe (the problem is reduced to rewiring equivalence classes, which are finite). In other words, we don’t give a normal form solution (although I tried hard to find one). In my dreams I was hoping we could instead find a short list of easily computed invariants which would detect rewiring equivalence, but that dream so far hasn’t been realized.

Posted by: Todd Trimble on February 22, 2008 2:58 PM | Permalink | Reply to this

Re: Logicians Needed Now

Oh, I hadn’t thought about the issue of exchange. Interesting!

I suspect it doesn’t ultimately affect what I was saying, but it does need to be dealt with somehow. One approach you sometimes see is to have a general permutation rule instead of the exchange rule, where any permutation of the formulae is allowed as a single step. Then it’s obvious that every proof is equivalent to one in which the permutation rule is never applied more than once in succession, because you can collapse successive permutations to their composite. Unless there’s something very subtle that goes horribly wrong if you do this, it would seem to deal with your concern.

The other approach is more radical, and is usually presented rather informally because the details get rather tiresome if you try to be spell them out. Instead of treating the left-hand side of a sequent as a list of formulae, treat it as a set of occurences of formulae. Athough as I say it’s a bit tedious to make this precise, I don’t believe there’s any intrinsic problem with the idea.

I too have spent some time thinking about the complexity of proof-equivalence for star-autonomous categories, and as far as I know the question is completely open. The best known algorithm (i.e. yours) is exponential, but the problem is not obviously NP-hard. (As usual, it’s the units that cause the trouble.)

Posted by: Robin on February 23, 2008 11:55 AM | Permalink | Reply to this

Re: Logicians Needed Now

I don’t believe there’s any intrinsic problem with the idea.

I don’t either (and in fact I had the same idea after posting). So you’re probably right; the only possible difficulty is spurious.

I too have spent some time thinking about the complexity of proof-equivalence for star-autonomous categories, and as far as I know the question is completely open.

I have some dim memory that the complexity of deciding whether there exists a proof ABA \vdash B in MLL for given formulas AA, BB was studied back in the 90’s [for some reason the names Scedrov, Lincoln, and Winskel come to mind], but deciding equivalence of proofs would seem to be rather a different matter. I’ve never looked at their stuff.

Posted by: Todd Trimble on February 23, 2008 1:54 PM | Permalink | Reply to this

Re: Logicians Needed Now

for some reason the names Scedrov, Lincoln, and Winskel come to mind

There is certainly work on the computational complexity of linear provability by, among others, Andre Scedrov, Patrick Lincoln and Timothy Winkler.

I find it remarkable that Constant-Only Multiplicative Linear Logic is NP-Complete, for example. (Lincoln and Winkler.) It shows forcefully how tricksy those units are: even when they’re all you have, they can still make trouble.

Posted by: Robin on February 23, 2008 7:40 PM | Permalink | Reply to this

Re: Logicians Needed Now

For what it’s worth, the complexity result I just alluded to is probably in

  • Max Kanovich, The multiplicative fragment of linear logic is NP-complete. Technical Report X-91-13, Institute for Language, Logic, and Information, June 1991.
Posted by: Todd Trimble on February 23, 2008 2:27 PM | Permalink | Reply to this

Re: Logicians Needed Now

Todd said:

In other words, we don’t give a normal form solution (although I tried hard to find one).

I’m sure some of you are aware of it, but it might be worth mentioning that Audrey Tan found such a normal form solution for the intuitionnistic case (MILL) in her thesis.

(And I never had access to Todd’s thesis, so I’m not sure what’s in there.)

The basic idea is that, using the natural orientation of \multimap’s, you may order the wirings, in such a way that there is always a maximal one, which you pick up for the normal form.

Posted by: Tom Hirschowitz on August 28, 2008 7:57 AM | Permalink | Reply to this

Re: Logicians Needed Now

Todd has a normal form solution for MILL in his thesis too, along very much the same lines (from what he’s told me).

I’m not sure how far to trust Audrey Tan’s claims. I seem to remember some local errors (false lemmas) in that section, but perhaps these are easily fixed? Have you worked through it in detail, Tom?

Posted by: Robin Houston on August 28, 2008 9:51 AM | Permalink | Reply to this

Re: Logicians Needed Now

I haven’t seen Audrey Tan’s thesis, but I know she has seen mine (I met her when I was visiting Cambridge in 1999); she was a student of Martin Hyland who also knows my thesis (and who I’d bet was the one who brought her attention to it). I’d be curious to see in what way her treatment differs from mine.

Posted by: Todd Trimble on August 28, 2008 12:12 PM | Permalink | Reply to this

Re: Logicians Needed Now

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?

Posted by: John Baez on February 29, 2008 11:06 PM | Permalink | Reply to this

Re: Logicians Needed Now

Also apparently missing is a rule for introducing II on the left.

Posted by: Todd Trimble on March 1, 2008 1:12 AM | Permalink | Reply to this

Re: Logicians Needed Now

Nice article!

One comment: I usually use the term “spin network” for what you call a “string diagram”, for obvious reasons. Unless I’m the only one who does this, maybe it would be good to mention the terminology “spin network” in the paper somewhere?

Dan

Posted by: Dan Christensen on February 22, 2008 10:01 PM | Permalink | Reply to this

Re: Logicians Needed Now

Good point! I only use ‘spin network’ when talking about representations of a group or quantum group, but I should mention this term as an alternative when I introduce the term ‘string diagram’. Other people say ‘Feynman diagram’.

Posted by: John Baez on February 23, 2008 2:28 AM | Permalink | Reply to this

Re: Logicians Needed Now

Is it easy to explain what the equivalence relation on proofs is?

The paper says that two proofs may induce the same function on hom-sets, so they should be regarded as equivalent, but aren’t the hom-sets already defined to be equivalence classes of proofs?

Posted by: Dan Christensen on February 23, 2008 3:00 AM | Permalink | Reply to this

Re: Logicians Needed Now

We say exactly what the equivalence relation must satisfy in Definitions 16 and 17 in Section 1.3.3. You’re reading the informal warmup section that’s supposed to get you ready for the serious stuff. I guess I need to put in something saying “we’ll tell you the details later”.

All the equivalence relations involved simply need to be generous enough to make sure we get a braided or symmetric monoidal closed category — that’s all!

(I’m willing to be corrected by our local experts, though.)

Posted by: John Baez on February 23, 2008 3:17 AM | Permalink | Reply to this

Re: Logicians Needed Now

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?

Posted by: Dan Christensen on February 23, 2008 3:37 AM | Permalink | Reply to this

Re: Logicians Needed Now

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!

Posted by: John Baez on February 23, 2008 4:19 AM | Permalink | Reply to this

Re: Logicians Needed Now

John, this blog review process of your paper is an amazing idea! There are some other category tutorial chapters for the book(s), which btw, will be entitled New Structures for Physics, including one by Eric Paquette and myself. Would you mind that also those go through the n-category filter process?

Posted by: bob on February 23, 2008 4:15 PM | Permalink | Reply to this

Re: Logicians Needed Now

Bob wrote:

John, this blog review process of your paper is an amazing idea!

It’s called ‘being too stupid to write an acceptable paper on time without publicly begging for help from all your friends’.

Actually, it’s a good idea even when you haven’t painted yourself into a corner. Feedback is always helpful. People usually email drafts to their friends. But when you get a public discussion going, more new ideas show up.

I think it was Urs Schreiber who first started doing this. I’ve been driven to it purely out of desperation.

There are some other category tutorial chapters for the book(s), which btw, will be entitled New Structures for Physics, including one by Eric Paquette and myself. Would you mind that also those go through the nn-category filter process?

That sounds like a great idea. You could either:

  1. email me a link to the paper and let me post a blog entry about it, or better
  2. email me a link along with some remarks you’d like to appear in the blog entry, or even better
  3. write a comment to the blog in the usual way, and preview it, but at the last minute don’t post it — instead, email the source to me. Then I can have it appear as a ‘guest post’ by you. The process of writing it as a comment and previewing it works out most of the bugs. If you do this, please tell me which ‘text filter’ you’re using.
Posted by: John Baez on February 23, 2008 6:19 PM | Permalink | Reply to this

Re: Logicians Needed Now

Here are a couple of comments.

Section 1.3.1.: Hilbert’s proof systems also have the rule called “generalization” which allows you to derive universal statements, see wikipedia. You should make it clear that you are talking about propositional calculus only.

Section 1.3.1.: Systems weaker than classical logic are not called “substructural”. A system is called “non-classical” if law of excluded middle is not valid in it. A particular example is “intuitionistic logic”. The “substructural” logics are those that fiddle with the structural rules of weakening and contraction. There is such a thing as “classical substructural logic” (i.e., a classical version of linear logic) so it really is a bad idea to introduce substructural logic the way you did. I would say instead something like: logicians study all sorts of logic that are not classical and seem strange to “ordinary” mathematicians. An example is “intuitionistic logic” (good to mention because most “ordinary” mathematicians “know” about it). Another example are so-called “substructural logics” in which one has to be careful about how hypotheses are used (for example, a hypothesis may be used at most once, or must be used exactly once).

Page 33, section 1.3.2 (why did you not number the pages?): I would say that the rules for smcc’s given on page 33 are not “a small fragment of classical logic” but rather “a small fragment of propositional calculus”, or just “a small fragment of logic”. There is no hint of classical in those rules. Then again when you comment on rules (c) you say “this is true in classical logic”, when you could just say “this is true in propositional calculus”. Maybe you keep saying “classical logic” to make it sound familiar to the reader? But then you should say “ordinary logic”, which will be even more familiar to the reader.

I would explain at the beginning of the section on logic that only propositional logic will be considered (it’s worth spending a sentence on explaining the difference between propositional and predicate calculus). Then I would not emphasize classical logic quite so much because you do not even talk about negation so the difference between classical and non-classical is invisible. “Substructural” and “classical” are linearly independent (but not quite orthogonal, I suppose).

Posted by: Andrej Bauer on February 24, 2008 5:15 PM | Permalink | Reply to this

Re: Logicians Needed Now

Thanks for the helpful comments, Andrej!

I didn’t number the pages because I’m using the style file provided by the folks who are compiling the book, and it doesn’t have page numbers. When I put a version of this paper on the arXiv it’ll have page numbers.

Since the audience will mainly consist of physicists, I kept saying ‘classical logic’ because I believe most of them will have no idea what the ‘propositional calculus’ or ‘predicate calculus’ are. I talk to mathematical physicists a lot and I hardly ever hear them use either of these terms. They won’t have much idea what ‘classical logic’ is, either — but they’ll probably guess it’s some kind of logic that isn’t quantum.

(For physicists, the main antonym of ‘classical’ is not ‘intuitionistic’, it’s ‘quantum’… and indeed the main reason I’m working with such a stripped-down formalism is that I want it to cover both classical and quantum situations: e.g., categories whose morphisms are proofs but also categories whose morphisms are Feynman diagrams.)

But, maybe I should do a bit more education! Maybe I should add some explanations of concepts like ‘propositional calculus’ and ‘predicate calculus’, and explain that we’re taking a very stripped-down approach and only touching on a tiny piece of the propositional calculus. The ‘overview’ subsection of the ‘logic’ section is very rudimentary so far, but today I plan to make it much longer, and that’s the place to correct these deficiencies.

Posted by: John Baez on February 24, 2008 7:44 PM | Permalink | Reply to this

Re: Logicians Needed Now

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).

Posted by: Andrej Bauer on February 24, 2008 9:20 PM | Permalink | Reply to this

Re: Logicians Needed Now

As I haven’t had time to read all the comments yet I don’t really know where to put this or where it fits in. Parts of this discussion (replacing infinite objects - or processes (as in analysis) by finite objects) reminds me of something I’ve been puzzled about for a long time. It is perhaps a bit philosophical, but it would be interesting to get some comments on it.

Take as an example a simple “infinite” (I’m not trying to be exact in phrasing things here) object like a real number. It is defined in terms of an infinite process (Cauchy …). However, the symbols, formulas, rules, whatever we write down on a piece of paper (or the words we utter) in order to convey this idea, are necessarily finite. Whether we call this syntactics or semantics is really just a play with words - in the end we need rules of manipulation of symbols. When we make a concrete calculation we use algorithms (finitely many steps on finite data types) whether with pen-and-paper or on a computer or by moving mechanical parts on some kind of “machine”. Thus it seems that mathematics in the final analysis is just “symbol shuffling”.

Yet there is something more to it. The symbols “mean” something. They actually aim at conveying ideas. Obviously one could easily take of on a tangent here and start to discuss Platonism et cetera. I don’t want to do this. Instead it seems to me that no formalism can really capture all aspects or properties of a mathematical idea. This works in two ways. There is necessarily a certain vagueness to mathematical concepts which we can often exploit creatively (by spotting analogies connections to other areas,…), but it also adds to the difficulty of understanding new maths especially if its done only by reading technical texts. On the other hand, if we only exploit what is explicit in the formalism, then we work as computers (raw computational power - but no understanding - no creativity).

Hope this wasn’t too off topic.

Posted by: Anders Bengtsson on February 26, 2008 1:06 AM | Permalink | Reply to this

Re: Logicians Needed Now

Thus it seems that mathematics in the final analysis is just “symbol shuffling”. Yet there is something more to it. The symbols “mean” something.

This is the syntax/semantics duality that has been discuseed here frequently. Perhaps the best explanation is here.

Posted by: Mike Stay on February 26, 2008 7:29 PM | Permalink | Reply to this
Read the post Physics, Topology, Logic and Computation: a Rosetta Stone
Weblog: The n-Category Café
Excerpt: Toward a general theory of systems and processes.
Tracked: March 11, 2008 7:46 AM
Read the post New Structures for Physics I
Weblog: The n-Category Café
Excerpt: Please comment on two chapters of a forthcoming book edited by Bob Coecke: 'Introduction to categories and categorical logic' by Abramsky and Tzevelekos, and 'Categories for the practicing physicist' by Coecke and Paquette.
Tracked: August 29, 2008 4:27 PM
Read the post New Structures for Physics II
Weblog: The n-Category Café
Excerpt: You can help review some more papers for Bob Coecke's New Structures for Physics.
Tracked: September 10, 2008 4:29 PM

Post a New Comment