Re: BV on display

Jon Cohen wrote:

> Hi again,
>
> Now that I am looking at this in the daytime, let me just point out that
> d1' (and by extension, d2') is not, in fact, properly displayed. The
> reason is, say we have a proof like so:
>
>
> X1 |- A   X2 |- B         A |- Y1    B |- Y2
> ------------------        -------------------
>  X1;X2 |- A<B              A<B |- Y1;Y2
>  ---------------------------------------
>              X1;X2 |- Y1;Y2
>
>
> Belnap's condition C8 says that we need to be able to reduce this to a
> proof which only uses display postulates and cuts on subformulae of A<B.
> We can do this in d1 as follows:
>
> X1 |- A   A |- Y1      X2 |- B   B |- Y2
> -----------------      ------------------
>    X1 |- Y1               X2 |- Y2
>   -----------(+)        ------------(+)
>   *Y1;X1 |- I             I |- Y2;*X2
>   ------------------------------------
>             *Y1;X1 |- Y2;*X2
>             ----------------
>               X1;X2 |- Y1;Y2
>
> What's the problem? The inference steps marked (+) implicitly used the
> display postulates for semicolon with a unit. We can't do this in d1'.
> Moreover, since we are not allowed to use the seq introduction rule (we
> can only use cut), there is no way of carrying out the reduction. 
>
>  
To add to the complication, I think we also need a rule like this
X |- Y ; Z
--------------
X |- Y, Z

This is needed (along with the associativity of seq) to prove
the structure
[<a; [b, c]>, <[~a, ~b] ; ~c>]
which I used to show the need of deep inference in BV.

I agree with you that d2' seems like the most likely candidate for 
displayed BV.
Splitting theorem might be easier to prove in d2' (on the surface at 
least) since
one does not need to deal with tensor (co-par) splitting, and the 
formula-judgment
distinction in displayed calculi might help as well.

-Alwen