Subject: Red and blue (again)
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-07-26 12:34:43 GMT (3 years, 49 weeks, 1 day, 17 hours and 1 minute ago)
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