Re: Cut-Elimination in Linear Logic

Philip Wadler <wadler@inf.ed.ac.uk> · Thu, 20 Nov 2003 10:07:26 +0100

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

Frank Pfenning wrote:

>   Literally, what you call "cut" in your example is not an instance of
> your cut rule, because the formulas "B" and "!B" do not match, ...

Whoops, I forgot to use !L before the cut.  I should have written,

                            ------Id              ------Id
                            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-o!B;|-;!B          !B;|-;!B otimes !B
    ------------------------------------------Cut
    A, A-o!B;|-;!B

Thanks for the citations!  -- P