Re: BV on display

Hi,

On Fri, 2005-08-05 at 02:45, Alessio Guglielmi wrote:
> I'm starting to get confused. 

Sorry, that's probably my fault!

> 1) I thought that deep inference can (sometimes?) be simulated in DC. 

It can, though it is not as straightforward as you might think. The
problem is with branching connectives, such as conjunction on the right.
One can't just pull this apart and stash a piece of it on the left,
since conjunction is not residuated in this way (and DC is all about
residuation/adjunction). Here's how it works in this case. Say I have
|-S{R}. So long as R is positive, its main connective must have been
introduced by a right introduction rule and, if the system is properly
displayed, then R must have been displayed at this stage. So, I can
travel up the proof tree to a point where I have S' |- R and
subsequently rewrite to S' |- T. Then, I can replay the moves I made
before by travelling back down the search tree and ending up with |-
S{R} (note that, in general, one needs to use a combination of display
postulates and this unravelling trick).

> This is clearly incorrect from the CoS point of view. The question 
> then seems to boil down to the following. How important is it to keep 
> I as a unit? 

Quite important. For instance, we need it in order to be able to derive
the rule that Alwen mentioned (namely, rewriting a semicolon to a
comma). If we have the DC-style q_ rule then we do this the same way as
in CoS:

X |- A;B
----------------
X |- [A,I];[I,B]
----------------
X |- <A;I>,<I;B>
-----------------
X |- A,B

>       O |- (a [b <R c>])
>      =====================
>       [-a O] |- [b <R c>]

This move is not really allowed in DC, for the reason I mentioned above.

> However, in CoS we have a much more general cut rule, and, in fact, 
> proving cut elimination in CoS is harder than in the sequent 
> calculus, and, most likely, in DC.

This is only a trick of the light. As I have mentioned previously, what
CoS does is remove the branch merging aspect of cut and have the right
conjunction do this. So, we can do the same in DC by using the rule:

X |- A & ~A
------------ (Cut')
X |- I

Lemma: Cut and Cut' are interderivable in a DC system.
Proof:
              A |- Y
             ---------         
             I |- *A,Y
            -----------
X |- A       I |- ~A,Y
-----------------------
    X |- A & ~A, Y
    -------------- (Cut')
      X |- I,Y
      --------
       X |- Y      


                      A |- A
                      -----------
                      A,*A |- I
                      -----------
  X |- A & ~A         A & ~A |- I
---------------------------------- (Cut)
              X |- I



> If we believe in the theory that there is no free lunch, how can we 
> hope to export DC technology into CoS, in cases like BV, where we are 
> able to prove cut elimination for a more general form of cut rule?

By the above lemma, we have cut elimination for Cut iff we have it for
Cut' - we have to pay full price for our lunch!

> In fact, Jon seems to suggest that the question might be reversed: 
> how to use splitting theorems in (generalised?) DC systems.

The point is that it seems unlikely that there is a DC system for BV
that is properly displayed, as I outlined in my previous email. I think
the reason is fundamental. What DC essentially does is keep the key
aspects that are needed in order to carry out a Gentzen-style cut
elimination proof. This is quite succesful if we limit ourselves to
relatively classical logics, predominantly those where everything
commutes nicely. However, the lack of sequentialisation theorems for
logics such as Pomset indicates that these logics may require a
substantially different cut elimination proof - well founded induction
on proof nets or the like. One technique out there is to place an
ordering on cut reductions considered as rewrite rules and prove that
this is terminating etc. However, this technique is at its core the same
as Gentzen's. 

In trying to obtain a general cut elimination theorem for DC which can
incorporate logics with weird noncommuting connectives, there is no
obvious way to extend Belnap's C8 condition. What appears to be
happening is that these sorts of logics do not fall victim to
traditional cut elimination proofs. Alwen's counterexample lends support
to this hypothesis.

Hopefully this email doesn't just confuse the issue more!

best,
Jon

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