Re: Red and blue (again)

On Thu, 28 Jul 2005, Alessio Guglielmi wrote:

> At 18:20 +0100 28/7/05, David J. Pym wrote:
> >The order of discovery is irrelevant.
> 
> Then, I don't understand your argument. Let me try and make a scheme 
> of what I understand, which shows why the order is relevant:
> 
> 1) There's LL sequent calculus, which happens not to induce 
> equivalence on coloured modalities.
> 2) People find models for it, which of course don't exhibit that 
> equivalence, either.
> 3) You say: it's good that the sequent calculus behaves that way, 
> because this is what the models suggest.

Furthermore: a category can have two non-isomorphic symmetric monoidal
structures.  Not only isomorphic: it's possible that there's no morphism 
at all from A tensor-red B to A tensor-blue B.

Yet MLL exhibits an equivalence between A tensor-red B and A tensor-blue
B.  

Of course, that apparent disparity is a consequence of the choice to
represent a model as a category rather than a multicategory, polycategory
or whatever, which would be closer to the syntax (albeit less convenient
for other purposes).  After all, as Lambek well knew (to echo David), a
multicategory can't have two non-isomorphic tensor products.

To expand on David's argument: for many of us, what makes us interested in
linear logic and similar systems in the first place is primarily the
models, not the proof theory (can I say that on this list?).  The order of
motivation (I'm interested in X, therefore I'm interested in Y) for an
individual may differ from the historical order.  And for us misguided
souls, it's clear that a cartesian product or even a tensor product are
universal constructions, whereas a comonad isn't.

Paul


-- 
Paul Blain Levy              email: pbl-dxBOTFGcEFw2EctHIo1CcQ@xxxxxxxxxxxxxxxx
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K.      tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl