On Sat, 11 Oct 2003, John Baez wrote:
On a related note: I've repeatedly heard people say something like "the multiplicative fragment of linear logic is the internal logic of (closed symmetric?) monoidal categories", but I've never heard a precise result along these lines. Has anyone worked out a sufficiently general concept of "the internal logic of a category" or "the internal logic of a certain 2-category of categories" so that one could take something like a monoidal category, or a symmetric monoidal category, or a closed symmetric monoidal category - or maybe the 2-category of all such - and extract by some systematic method the corresponding "internal logic"? I'm vaguely imagining some class of generalizations of the Mitchell-Benabou language of a topos, or something like that - but I'm really interested in the nonCartesian case.
Hi John - You might want to take a look at the paper by Robin Cockett and me "Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories " in TAC Vol 3 No 5. ftp://ftp.tac.mta.ca/pub/tac/html/volumes/1997/n5/n5.ps As for a general theory - there are plenty of examples, though I don't know if anyone has really made a general theory of this notion of a categorical doctrine, often referred to, and based on a paper of Kock and Reyes from the 70's. But there are many examples (many in the papers Robin and I have written on linearly distributive categories and related structures - visit my webpage if you're interested), which make clear how to go from the internal logic of a category to the category and back. I suggest also you look at our "Introduction to linear bicategories" (MSCS:10(2000)2 pp 165-203), also available on my webpage, for a higher dimensional approach. - all the best, Robert -- <rags@math.mcgill.ca> <www.math.mcgill.ca/rags>