Subject: Re: BV on display
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-08-04 16:45:20 GMT (3 years, 47 weeks, 6 days, 12 hours and 35 minutes ago)
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