Hi Alwen,

> If I understood your system correctly, I think it actually proves more
> formulas (or structures) than BV.  

You're absolutely right. I was trying to cook up a system wherein the q_
rule comes about as a result of the seq introduction rules, rather than
explicitly stating it. There seem to be a few distinct logics floating
around here. Let's call the system consisting of the display postulates
exactly as I gave them before together with the following seq
introduction rules d1:

 
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

This is the original system I started with and I am pretty sure that it
does not capture all of BV, since I can't find a way to make it simulate
the proof of your counterexample (essentially, it has trouble applying
the q_ rule deeply). We can fix this by explicitly adding in the q_ rule
and its dual:

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

Let's call this system d2 and let's also go crazy and call the system
from my previous email d3. For a given di, let's say that di' is the di
with the display postulates for the semicolon restricted to non-units.

If D and D' are two calclui, let D < D' mean that the set of provable
structures of D is contained in that of D'. Then, we have the following:

d1 < d2 = d3

The example you gave shows that we also have di' < di.

What I believe is that BV = d2' and that d2' \ne d3'. I'm fairly
confident that all of these relations are true, though it is pretty late
this end of the world so I haven't checked it properly yet.

best,
Jon

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