Re: quantum logic

[Robert Seely <rags@math.mcgill.ca>]

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>