quantum logic

["John Baez" <baez@math.ucr.edu>]

Dear Categorists -

Do any of you know particularly insightful treatments of
quantum logic via category theory?  I'm more or less familiar
with quantum logic as the theory of the complete orthocomplemented
lattice of closed subspaces of a given Hilbert space.  But now I'm
interested in developing quantum logic starting as much as possible
from general properties of and structures on the category of
Hilbert spaces and bounded linear maps - for example, the fact
that it's an abelian category, and becomes a *-category and symmetric
monoidal category in a nice way (with Hilbert tensor product as the
monoidal structure).  And I'm interested in things like how the
2-dimensional Hilbert space acts a bit like a subobject classifier.

I don't mind sticking with finite-dimensional Hilbert spaces for now
to avoid certain subtleties.

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.

The reason I ask this is that it would be nice if you could
throw the (closed, symmetric, monoidal, *, etcetera...) category
of Hilbert spaces into some big machine and have "quantum logic"
pop out - and then throw in other similar categories, and have other
kinds of logic pop out.

Best,
jb