BV on display

Hi all,

At Alessio's prompting, I'll outline how to capture BV in a display
calculus (DC), in the process showing how Alwen's counterexample goes
through.

Since it is easy to do MLL+Mix in DC, I'll focus only on the seq
connective. Note that Mix need not be explicitly stated in a DC system,
since it is automatic by the display property. Remember that the seq
connective is denoted in CoS by <R;T> and its behaviour in BV is
governed by the rule:

    S<[R,T];[U,V]>
q_  -------------- 
    S[<R;U>,<T;V>]

Squinting at this rule, one interpretation of what it does is the
following:

<R |- T  ; U |- V>
-------------------
  <R;U> |- <T;V>

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

The introduction rules for seq are (note that it is a *comma* on the
structural side, not a semicolon):

X |- A    Y |- B       A |- X   B |- Y
----------------       ---------------
   X,Y |- A<B             A<B |- X,Y

A;B |- X           X |- A;B
=========          ========
A<B |- X           X |- A<B

For the rest of this post, I'll use ; exclusively, even where I really
ought to use <. This shouldn't cause any confusion, since they are
really the same thing. Additionally, I'll use "I" to simultaneously
denote the unit of conjunction, disjunction and seq in the DC system
(the same as o in BV).

Definition: The standard DC rules for MLL + Mix together with the above
rules is called dBV.

Theorem: dBV has cut elimination.
Proof: It is properly displayed.

Theorem: A structure is provable in dBV iff it is provable in BV (modulo
the obvious translation between CoS and DC structures). 
Proof: 

The only hard part is showing that every theorem of BV is also a theorem
of dBV. We need to derive the q_ rule but doing this in one step is
messy. Instead, let's first show that the following is derivable:

X |- A;(B,C)
------------
X |- (A;B),C

To do this, assume that we have a derivation, D, of the numerator. WLOG,
the right-hand semicolon was introduced by the last inference in D.
There are two possibilities: either it was introduced by a display
postulate or it was introduced by the right seq introduction rule. I'll
only consider the latter, the proof for the former is similar. In this
case, we must have X = X1,X2 as well as derivations of X1 |- A and X2 |-
B,C. Building from here, we have:

            X2 |- B,C
           ------------
X1 |- A    X2, *C |- B
-----------------------
  X1, X2, *C |- A;B
  ------------------
   X1,X2 |- (A;B),C     =   X |- (A;B),C

Now, assume that we have a derivation of X |- (A,B);(A',B'). Using the
rule we just derived numerous times, we get:

X |- (A,B);(A',B')
-------------------
X |- ((A,B);A'), B'
-------------------
X |- ((B,A);A'), B'
-------------------
X |- B, A;A', B'
------------------
*B |- B', *X, A;A'
--------------------
*B;I |- B', *X, A;A'
-----------------------
I |- B;(B', (*X,A;A'))
-----------------------
I |- B;B', *X, A;A'
-------------------
X |- A;A', B;B'

---------------------------------------------------------------
                                                
Corollary: BV has cut elimination.
Proof: It is easy to see that cuts in BV correspond to cuts in dBV and
vice versa. The corollary then follows from the previous two theorems. 


Intuitively, the branching introduction rules take care of shallow
applications of q_, while the deep applications of q_ are handled by the
display postulates. Since we have derived the q_ rule (and, by duality,
the correpsonding q^ rule for the LHS of the dBV system), we can
directly simulate Alwen's proof. That is, every time the q_ rule is used
deeply in a BV proof, the corresponding application in the dBV system
comes about by "unwrapping" the cedent via the display postulates,
applying the derived q_ rule in dBV and finally "rewrapping" the cedent.

Thanks to Alwen, we can now say that when it comes to provability, DC is
a nontrivial extension of the sequent calculus!

best,
Jon

-- 
http://rsise.anu.edu.au/~jon