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-/[email protected] 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