Re:Red and blue (again)

At 09:10 +1000 27/7/05, Rajeev.Gore-/hejbHI7ObxcYUQs2IXCwA@xxxxxxxxxxxxxxxx 
wrote:
> > 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.
>
> Not sure what you mean here Alessio. What is wrong with translating 
> into a fixed meta level ? The problem with traditional sequent 
> calculi is that they have no meta-level connective for box at all.

There is nothing wrong, technically, in translating into a fixed meta 
level. However, what is the point in asking the question about 
equivalence of differently coloured connectives, when the meta level 
is fixed? I mean, instead of saying

   red-box = blue-box

plain and simple, one says

   red-box = meta-box   &   blue-box = meta-box   ->   red-box = blue-box .

I say: what the @%#$???

Perhaps we agree that new logics are needed with very different 
semantics from classical logic. If we want to deduce and compute in 
these logics, we need a syntax which is as neutral as possible 
regarding semantics. In this perspective, keeping a fixed meta level 
is a methodological and strategical mistake, because it limits the 
possibilities tremendously.

Asking the colour question means asking a purely syntactic question 
related to the `interaction' of subformulae in a proof. This means 
forgetting about the semantics (and associated notion of equivalence) 
and trying to reconstruct it in part. If you do so by resorting to a 
meta level that keeps with it the old classical equivalence, then 
you're setting up a conceptually dubious experiment, don't you agree?

The case of linear logic is exemplary. Somehow, with some tricks, 
linear logic's sequent system manages to capture the exponentials, 
but it fails the colour blindness test, which is an indication of 
stressing the limits of a biased syntax. The problem, as you say, 
might be the lack of a meta-level box. However, if you fix the 
problem by adding the box, you'll have another problem next time you 
need something different. Much better to get rid of the meta level 
entirely, since you can solve the colour problem *and* get a better 
syntax in addition, like a local rule for promotion instead of a 
global one, many more normal forms, lack of bureaucracy, etc.

By the way (contrary to all of Girard's blah blah about mixing 
semantics and syntax) I believe that the objective of finding a 
formalism, with good combinatorial properties, which is as 
independent of any semantics as possible, is a nice conceptual and 
mathematical problem. It's a bit like finding an elegant, universal 
model of computation, like the lambda calculus.

At 11:19 +1000 27/7/05, Jon Cohen wrote:
> 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...

I did it on purpose, I wanted to have a lattice style rule on the 
right just to make clear that we are talking about classical logic, 
but I didn't want to show contractions on the left, which are not the 
point. I'm not concerned about cut elimination here (besides, I'm not 
telling you the other inference rules).

> 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...

I think we all agree that you can modify the sequent calculus (by 
colouring commas and branches, for example) in such a way that, in 
this particular case, it behaves like CoS. However, this is not the 
point. The goal of the colour-blindness experiment is to see whether 
equivalence can be proved in the sequent calculus *as is*.

It seems like people attach importance to the outcome of the 
experiment (success for conjunction, failure for modalities, for 
example). However, the existence of another proof theory (for 
example, CoS), where the outcome of the experiment can be chosen at 
will, shows that the experiment only reveals an artifact of the 
sequent calculus. This is my point.

> Your argument against SC seems to hinge on the fact that it cannot 
> show two colours of exponentials to be equivalent.

No, what I'm saying is that in the SC you cannot choose, while in 
deep inference you can choose *any* outcome of the experiment (and 
not just equivalence/non-equivalence, but varying degrees of it). In 
other words, attaching importance to the experiment is, no more and 
no less, committing to a particular meta level, which might not be 
obvious to people doing the experiment.

> 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 depends on the inference rules you choose. If you just colour the 
rules you have for a colour-less system (say, Phiniki's S5, or Lutz's 
linear logic), then you *don't* get the equivalence, and not just for 
the modalities, but for every connective.

If you do want to get the equivalence (for any connective), you can, 
by adding rules (that don't necessarily introduce it explicitly).

> 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).

I completely agree with you, and this is my point: the presence or 
lack of the equivalence should be a consequence of the logic, not of 
the formalism used to represent that logic.

This is the problem with the sequent calculus and its descendants: 
you cannot completely separate what is logical from what is 
bureaucracy of the formalism.

-Alessio