Re: Red and blue (again)

> In linear logic, this works for all connectives but not for the 
> modalities: differently coloured modalities are independent, they 
> aren't equivalent.
Well that's good.

Mathematical models of linear logic's proof theory (MLL!, for simplicity)
are given by monoidal categories (for tensor, implication, etc) with a
monoidal co-monad for the exponential, ! .

There is no reason why (the co-algebras for) two different monoidal 
co-monads
should be equivalent. So it would be unfortunate if there 
axiomatizations were
equivalent (no completeness, for one thing).

David

--
Prof. David J. Pym                Telephone: +44 (0)1 225 38 3246
Professor of Logic & Computation  Facsimile: +44 (0)1 225 38 3493
University of Bath                Email: 
d.j.pym-+E0FUbDlCk21Qrn1Bg8BZw@xxxxxxxxxxxxxxxx
Bath BA2 7AY, England, U.K.       Web: http://www.bath.ac.uk/~cssdjp 

Royal Society Industry Fellow, HP Labs, Bristol: david.pym-VXdhtT5mjnY@xxxxxxxxxxxxxxxx 

--
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed.