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