Red and blue (again)

Hello Dale and batrachianologists,

a few years ago Dale mentioned to me this phenomenon: if you paint 
connectives in the sequent calculus in red and blue, you can often 
prove their equivalence. For example, if you have red conjunction &-R 
and blue conjunction &-B, subjected to the same rules, then you can 
prove that

   F  &-R  G   <->   F  &-B  G  .

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

We discussed this thing a few times already, also on Frogs, but I 
never resolved to write down a couple of paragraphs. So, since the 
thing resurfaced again at Dale's talk in Lisbon, I wrote a quick note 
with my point of view: 
<http://iccl.tu-dresden.de/~guglielm/p/AG15.pdf>.

In brief: this phenomenon is another artifact of the sequent calculus.

The first thing I have to say is that colouring connectives in red 
and blue is a purely syntactic thing, not necessarily connected to 
any meaningful semantics. Still, I agree that the relation of this 
with equivalence is interesting.

Second: my immediate reaction would be that if two things only are 
distinguished by the colour, but they behave the same, they must BE 
the same! So, this seems to me a (rare) case in which semantics 
should religiously follow syntax.

However, what happens in the sequent calculus is only by coincidence 
the right thing. If one looks closely, one sees that the equivalence 
is only the consequence of some strong bias towards classical logic. 
If differently coloured connectives are all reduced to the SAME meta 
level (the classical one), then, OF COURSE, one gets equivalence. 
And, OF COURSE, equivalence is missing when there is no meta level 
corresponding to the connectives, like in the case of linear logic 
modalities.

So, the sequent calculus is only apparently half-adequate to deal 
with the situation, and I guess the same is true with every formalism 
which commits to a fixed meta level, like hypersequents and the 
display calculus.

In deep inference there is no meta level, and in fact there is no 
difference between modalities and the other connectives, in linear 
logic or otherwise. However, one can always get the equivalence, 
provided one is very specific on what `behaving the same' means.

For me this is a confirmation that the right thing for a syntactic 
formalism is to be completely agnostic about the semantics, what the 
sequent calculus clearly is not.

Anyway, let me know what you think, the note is extremely simple and 
non-technical.

Ciao,

-Alessio