Re: Cut-Elimination in Linear Logic

Philip Wadler <wadler@inf.ed.ac.uk> · Fri, 21 Nov 2003 10:11:03 +0000

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Thanks to Frank and Sanjiva for replies.

In the example I gave, Cut elimination can be performed by commuting
the right-hand tree to the top of the left-hand tree.  This is
possible because the Cut is against a side-formula in the right-hand
tree.  (A Cut against a formula of the form !B must be against a
side-formula or against the principle formula of !R, and the latter
case is easy.)

                                B;|-;B                B;|-;B
                                ------------Dereliction      
------------Dereliction
                                ;B|-;B                ;B|-;B
                                --------------!R              
--------------!R
                                ;B|-;!B               ;B|-;!B

----------------------------------------------------------otimes-R
    A;|-;A    !B;|-;!B          ;B|-;!B otimes !B
    ------------------------------------ -oE       
------------------------------------!L
    A,A-o!B;|-;!B               !B;|-;!B otimes !B

------------------------------------------------------------------------ 
--------------------Cut
    A,A-o!B;|-;!B

becomes

                B;|-;B                B;|-;B
                ------------Dereliction     ------------Dereliction
                ;B|-;B                ;B|-;B
                --------------!R             --------------!R
                ;B|-;!B               ;B|-;!B

----------------------------------------------------------otimes-R
                ;B|-;!B otimes !B
                ------------------------------------!L
    A;|-;A      !B;|-;!B otimes !B
    ------------------------------------------------------------ -oE
    A,A-o!B;|-;!B otimes !B

> I think I understand what LU fragment you're looking at  
> (Neutral+Positive
> Int. Logic), so I think it it somewhat incorrect to say you don't
> have polarities -- you have !A, which is positive.
> I guess you mean that all atomic formulae are of neutral polarity,
> and all positive formulae are obtained by the !-L and !-R rules.

What I meant is that I did not include Girard's rules which refer to  
the polarities:

    G;G'|-D',N;D
    ------------------------
    G;G'|-D';N,D

    G;P,G'|-D';D
    ------------------------
    G,P;G'|-D';D

where N has negative polarity and P has positive polarity.
Frank does not have these in his system LV, which is a variant of LU.
So far as I can see, these rules don't allow you to derive more  
sequents.
Instead, their purpose is to allow the classical connective A wedge B,
which is roughly the same as !A otimes !B, to be given a definition that
is clearly associative.  Is that right?

Cheers,  -- P