Re:Red and blue (again)

Addition. Sorry, but I just saw a point that cries for being set straight.

As I said already, I believe that if blue and red connectives behave 
the same, then they should be equivalent, and that I think that this 
is one of the few cases where semantics should religiously follow 
syntax/behaviour.

At 09:42 +1000 28/7/05, Rajeev.Gore-/hejbHI7ObxcYUQs2IXCwA@xxxxxxxxxxxxxxxx 
wrote:
>  > 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:

No! There is a much simpler reason: these two rules actually don't 
specify the same behaviour. In fact [red] behaves with [red] in a 
different way than [blue] behaves with [red], and the other way round.

If you really want to state that red and blue behave the same, you 
have to further add the rules

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

which of course gives you the equivalence (it states it!).

The mistake here comes from our (hard-wired, built-in) attitude to 
consider behaviour as implicitly specified by the meta-level. For 
this reason I think my argument with CoS works well, because in CoS 
you're forced to do without the meta level, behaviour can be no more 
than what you see.

Side remark: I always thought that the value of the meta level is in 
providing some `philosophical meaning' to the inference rules. What 
would be the philosophical meaning of red and blue blobs, commas and 
branches? Going that way is just technological overkill, I think.

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

-Alessio