Re:question on formalism B

At 11:10 +0100 15.3.05, Lutz Strassburger wrote:
> I guess that
>
>    ([A,B],[C,D])
> s ---------------
>    [A,(B,[C,D])]
> s ---------------
>    [A,[(B,C),D]]
>
> vs.
>
>    ([A,B],[C,D])
> s ---------------
>    [([A,B],C),D]
> s ---------------
>    [[A,(B,C)],D]
> = ---------------
>    [A,[(B,C),D]]
>
> should be the typical example. The two derivations above are 
> identified by proof nets. But not by B, are they? Am I right or 
> wrong about this?

Right. In wired deduction, you have

     ([A  B] [C  D])             ([A  B] [C  D])
    s =|==|===|  |=           s   =|  |===|==|=
      [| (|  [|  |])]           [([|  |]  |) |]
    s  | =|===|==|=     vs.   s   =|==|===|= |  ,
      [A (B   C) D  ]           [  A (B   C) D]

and you cannot transform one derivation into the other simply by 
moving the horizontal bars up and down. (One could notice that we 
could permute the pipes, but it's easy to build examples on top of 
this where the permuting wouldn't work any more.)

Of course, this is a patent case of bureaucracy, if we consider the 
two proofs morally the same. However, this is an example of 
bureaucracy in the deductive system, not in the formalism. In this 
case, we can fix the deductive system by simply adding the local rule

      ([B A] [C D])
   ss  =|===X===|=  .
      [(B C)  A D ]

It would be interesting to find geometric and at the same time 
deductive ways of coping with a situation like this one.

-Alessio