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
