Re: Red and blue (again)

Hi,

First, there's a slight mistake in the note - it uses the lattice style
introduction rule on the right and the monoid style rule on the left.
This breaks cut elimination...

More to the point, I don't see the issue here. We need to remember a
couple of quirks of CoS - namely that it is a one sided calculus and
that [,] takes the place of comma (since we are working on the right).
If you introduce two colours of [,], then this is, as you say, just the
same as introducing two colours of comma. How to distinguish between two
"colours" of branching? Going up a proof, it is obvious. Coming down, it
just means that we have two conjunctions to choose from - just like if
we have access to both lattice and monoidal conjunction (and are working
in linear logic where they are distinct notions). This issue does not
arise in CoS because it keeps track of the type of branching by using
different colours for (,). This is even clear when one asks how to
introduce (,) in a CoS proof...

Your argument against SC seems to hinge on the fact that it cannot show
two colours of exponentials to be equivalent. However, when moving to
CoS you only dealt with the classical connectives. Can CoS prove the
equivalence of {!}A and <!>A? Here, the different braces indicate the
different colours. If so, then this is quite worrying!

It is not always desirable for different coloured modalities to be the
same. For instance, in, say, basic tense logic Kt, we have a modality
for each of future and past. We certainly don't want them to come out to
be equivalent. Here, the fact that the modalities are different has
*everything* to do with the logic. But this is just the same as if we
had different coloured bangs (!) in linear logic, since these are just
S4 modalities (that is, if we wanted the "colours" to interact sensibly,
we would really be working in KtS4).

best,
Jon

-- 
http://rsise.anu.edu.au/~jon