Re: BV on display

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. 

One way to try squirm out of this situation is to postulate a mix-like
rule for semicolon in d1' but it's not a good fix - Belnap's C8
condition still does not want to go through (and C8 is where the real
meat of Belnap's conditions lies).

I still feel that d2' proves the same structures as BV. However, there
are subtle issues here, since Belnap's theorem does *not* apply (for the
above reasons), so we cannot automatically conclude cut elimination for
d2'. However, we know that BV has cut elimination and it is not hard to
show that, assuming the systems prove the same structures, then one has
cut elimination iff the other one does. It seems that one could still
cook up a traditional cut elimination proof for d2', but it may be worth
investigating what splitting means in the display context. Note that
Belnap's proof is very close in spirit to Kai's atomic cut elimination
proof.

What is clear is that Belnap's conditions are not the most general
possible and it seems that we need to do a major reworking in order to
obtain a general cut elimination theorem that incorporates
noncommutative connectives, such as seq.

best,
Jon

On Thu, 2005-08-04 at 00:20, Jon Cohen wrote:
> 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