Re: BV on display

Hi Jon,

>In other words, it merges branches, keeping track of which branch is on
>the  left and which is on the right. It turns out that this isn't
>*quite* the rule we want in our DC system, for reasons that I won't go
>into. Anyway, let's settle on notation. I'll use a semicolon for the
>meta-level seq connective and < for the object level one. The semicolon
>satisfies the obvious display postulates:
>
>X;Y |- Z        X;Y |- Z        X |- Y;Z     X |- Y;Z
>=========       ========        ========     ========
>X |- Z;*Y       Y |- *X;Z       *Y;X |- Z    X;*Z |- Y
>
>  
>
If I understood your system correctly, I think it actually proves more
formulas (or structures) than BV.  For instance, consider the following 
proof

a |- a
-------
a;I |- a
--------
I |- *a ; a

I think the display postulates above need to be strengthened a bit,
for instance, with a proviso that Y is not unit. Although I don't know
how it would affect the completeness proof.

Best regards,
-Alwen