Re:Red and blue (again)

> 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 @%#$???

Agreed.

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

Absolutely.

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

Yes.

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

This is one solution.

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

But display logic also give you this freedom. Instead of turning red
boxes and blue boxes into black blobs (say) at the meta-level, you can
turn red boxes into red blobs and blue boxes into blue blobs. Now the
equality fails unless you postulate rules that allow you to turn blue
blobs into red ones and vice versa. That is, you have all the freedom
that you want to choose our outcome at will. In fact, a little thought
shows that the ability to turn blue/red blobs into red/blue blobs is
just a set of equations: but they live at the meta-level, not at the
object level. 

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

Ditto for DL. Just choose different meta-level connectives. In fact,
in DL, you can even break residuation in a controlled way by using
different flavours of meta-level commas, blobs etc. see the SLD paper.

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

There is an argument in favour of being able to prove equivalence. The
sequent calculus is supposed to capture all essential properties of a
connective. So if we have two connectives & and /\ say which have
identical introduction rules on both sides, then surely they should be
provably equivalent.

It is often claimed that the rules for modalities like [] and <> do
not do this. So we can have two boxes with rules like:

      X ==> P                          X ==> P
  --------------                  ---------------------
   [red] X ==> [red] P            [blue] X ==> [blue] P

The claim is that they should now be provably equivalent. These rules
fail this test.

But that is because there is implicit weakening hidden in these rules:
they should really be of the form:

                   X ==> P
   ------------------------------------------------------------------
      Junk1, [red] X, [blue] Y ==> [red] P, [red] Z, [blue] W, Junk2

and similarly for the blue rule.

Now, these rules are not "the same" and so it is only right that the
equivalence test fails. In other words, there is nothing wrong with
the sequent calculus.

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

But if the formalism captures the logic exactly, and these
equivalences do/don't hold in the logic then they should/not hold in
the formalism either.

That is, suppose that red means future and blue mean past. Then there
is an adjunction between them of the form 

    P --> [future]<past>P and its mirror.

If your sequent calculus does not capture this then it does not
capture your logic properly. If it does, then you will be able to
prove this part of the "equivalence". If you then add symmetry so they
really are equivalent then this equivalence will come about by being
able to prove symmetry. This is certainly possible in the sequent
calculus (although perhaps not in a cut free manner for S5).

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

Hmmm .... not convinced yet ...

raj