Re: BV on display

Hello,

I'm starting to get confused. I thought I had reached some 
conclusions, but then the recent emails by Jon and Alwen made me 
think again. May I ask two general questions? I would have more, but 
these two questions are, I think, rather important if one wants to 
transfer any technology from DC to deep inference.


1) I thought that deep inference can (sometimes?) be simulated in DC. 
The CoS scheme for deep inference asks for rules of the kind

      S{R}
   r ------ ,
      S{T}

and the obvious DC translation would be something like

      |- S{R}
     =========
      *S |- R
   r ---------
      *S |- T
     ========= .
      |- S{T}

Here, the first and last === bars stand for several applications of 
display postulates, and *S stands for S{ } `inside out and dualised'.

Alwen's observation seems to suggest that the * operation is not as 
obvious as it seems. He observes:

At 15:31 +0200 3/8/05, Alwen Tiu wrote:
> a |- a
> -------
> a;I |- a
> --------
> I |- *a ; a

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? If all one wants to do is getting *S, then one only 
needs to record where `outside' is in *S. I will explain with an 
example. Suppose I want to access R inside S{ } = (a [b <{ } c>]); 
then, given that the `mark' O means `outside', I can do

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

Of course, O is not a unit for anything, because I need it to mark 
where the outside is (I've read somewhere that this is what happens 
when you approach a black hole: the inside becomes outside).

Anyway, the question is whether this is what we want and whether not 
using I for this purpose is a problem (regarding general cut 
elimination, for example). (One immediately should ask himself 
whether all this black-holing is really necessary compared to just 
going inside formulae and deduce, but it's another question...)


2) This one is quick. It seems like what DC has to offer to CoS is a 
general cut elimination theorem that only requires checking some 
`local' conditions on inference rules. I don't know this theorem in 
sufficient detail, but, after looking at Belnap's papers, it seems to 
me that the theorem works for a shallow, i.e., normal, version of the 
cut rule.

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.

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?

In fact, Jon seems to suggest that the question might be reversed: 
how to use splitting theorems in (generalised?) DC systems. Of 
course, I would be proud to contribute something to the DC theory, 
but then, really, one should ask whether it is worthy to apply a 
difficult technique (splitting) to a complicated system (e.g., BV in 
DC).


Can you help with these questions? Ciao,

-Alessio