Re: Red and blue (again)

At 15:54 +0100 28/7/05, David J. Pym wrote:
>>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 their axiomatizations were
>equivalent (no completeness, for one thing).

If I'm not terribly mistaken, these models were found *after* the 
definition of linear logic's sequent calculus. In that case, I don't 
see your point. I mean: if the properties of the sequent calculus of 
linear logic were different, people would have had to look for 
different complete models.

You could make the same argument with phase semantics, but, again, 
it's a semantics that came afterwards, meaning that it simply tries 
to catch up with the syntax (I almost completely agree with Giorgi on 
these matters).

Anyway, I agree that the fact that differently coloured modalities of 
linear logic are not equivalent is good, simply because they don't 
behave the same way if you just colour the modalities rules, as I 
argued in my answer to Raj.

-Alessio