headers
Jon Cohen | 3 Aug 2005 13:36
Picon
Picon

BV on display

Hi all,

At Alessio's prompting, I'll outline how to capture BV in a display
calculus (DC), in the process showing how Alwen's counterexample goes
through.

Since it is easy to do MLL+Mix in DC, I'll focus only on the seq
connective. Note that Mix need not be explicitly stated in a DC system,
since it is automatic by the display property. Remember that the seq
connective is denoted in CoS by <R;T> and its behaviour in BV is
governed by the rule:

    S<[R,T];[U,V]>
q_  -------------- 
    S[<R;U>,<T;V>]

Squinting at this rule, one interpretation of what it does is the
following:

<R |- T  ; U |- V>
-------------------
  <R;U> |- <T;V>

In other words, it merges branches, keeping track of which branch is on
the  left and which is on the right. It turns out that this isn't
*quite* the rule we want in our DC system, for reasons that I won't go
into. Anyway, let's settle on notation. I'll use a semicolon for the
meta-level seq connective and < for the object level one. The semicolon
satisfies the obvious display postulates:
(Continue reading)

Permalink | Reply | 7 comments |
headers
Jon Cohen | 3 Aug 2005 16:20
Picon
Picon

Re: BV on display

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
(Continue reading)

Permalink | Reply | 5 comments |
headers
Alwen Tiu | 3 Aug 2005 15:31
Picon
Favicon

Re: BV on display

Hi Jon,

>In other words, it merges branches, keeping track of which branch is on
>the  left and which is on the right. It turns out that this isn't
>*quite* the rule we want in our DC system, for reasons that I won't go
>into. Anyway, let's settle on notation. I'll use a semicolon for the
>meta-level seq connective and < for the object level one. The semicolon
>satisfies the obvious display postulates:
>
>X;Y |- Z        X;Y |- Z        X |- Y;Z     X |- Y;Z
>=========       ========        ========     ========
>X |- Z;*Y       Y |- *X;Z       *Y;X |- Z    X;*Z |- Y
>
>  
>
If I understood your system correctly, I think it actually proves more
formulas (or structures) than BV.  For instance, consider the following 
proof

a |- a
-------
a;I |- a
--------
I |- *a ; a

I think the display postulates above need to be strengthened a bit,
for instance, with a proviso that Y is not unit. Although I don't know
how it would affect the completeness proof.

Best regards,
(Continue reading)

Permalink | Reply | 6 comments |
headers
Jon Cohen | 4 Aug 2005 08:19
Picon
Picon

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.
(Continue reading)

Permalink | Reply | 4 comments |
headers
Alessio Guglielmi | 4 Aug 2005 18:45
Picon
Favicon

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:
(Continue reading)

Permalink | Reply | 2 comments |
headers
Rajeev.Gore | 5 Aug 2005 01:13
Picon
Picon

Re: BV on display


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

If this is not what you want then you need to use different units.
Then introduce some discipline to sort out when the units should
behave in certain desired ways. You are trying to do too much with
just one unit.

> 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.

The theorem and the rule has to be considered in conjunction with the
display property. Although it is a shallow cut rule, the display
property does give us some aspects of deep inference (all aspects if
you believe Jon's ranting :)

> 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 possible but I can offer no insights.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jon Cohen | 5 Aug 2005 06:00
Picon
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alwen Tiu | 4 Aug 2005 15:38
Picon
Favicon

Re: BV on display

Jon Cohen wrote:

>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
>
(Continue reading)

Permalink | Reply | 0 comments |

Gmane