Cut-Elimination in Linear Logic

Philip Wadler wadler at
Thu Nov 20 10:07:26 EST 2003

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

Thanks for the citations!  -- P

More information about the Types-list mailing list