Cut-Elimination in Linear Logic (was: (no subject))

[Frank Pfenning]

Hi Phil,

  the question is addressed in

Frank Pfenning. Structural cut elimination in linear logic. Technical
Report CMU-CS-94-222, Department of Computer Science, Carnegie Mellon
University, December 1994.
http://www.cs.cmu.edu/~fp/papers/cutlin94.pdf

  A newer paper treating the intuitionistic case (and natural
deduction):

A Judgmental Analysis of Linear Logic
Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning.
Technical Report CMU-CS-03-131, April 2003.
http://www.cs.cmu.edu/~fp/papers/jill03.pdf

  This second paper is currently under revision, but as far as
cut-elimination is concerned it is close enough.

  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, but you
can see from the above papers how this can be fixed.

  - Frank

> Date:    Wed, 19 Nov 2003 13:21:02 +0100
> To:      types at cis.upenn.edu
> CC:      Philip Wadler <wadler at inf.ed.ac.uk>
> From:    Philip Wadler <wadler at inf.ed.ac.uk>
> Subject: (no subject)
> 
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> I have a basic question about the system LU, as introduced by:
> 
>    J.-Y. Girard, On The Unity of Logic,
>    Annals of Pure and Applied Logic 59:201--217, 1993.
> 
> I need here only a small fragment of the system, and do not require
> polarities.  Write G for Gamma, D for Delta, L for Lambda, P for Pi.
> 
> Sequents have the form:
> 
>    G; G' |- D'; D
> 
> Weakening and contraction apply to G' and D', but not G and D.
> 
> Here are some of the rules:
> 
>    ------Id
>    A;|-;A
> 
>    G;G'|-D';D,A   A,L;G'|-D';P
>    ---------------------------Cut
>    G,L;G'|-D';D,P
> 
>    G,A;G'|-D';D
>    ------------Dereliction
>    G;A,G'|-D';D
> 
>    ;G'|-D';A
>    ----------!R
>    ;G'|-D';!A
> 
>    G;A,G'|-D';D
>    -------------!L
>    G,!A;G'|-D';D
> 
> Consider the following proof
> 
>                            ------Id              ------Id
>                            B;|-;B                B;|-;B
>                            ------Dereliction     ------Dereliction
>                            ;B|-;B                ;B|-;B
>                            -------!R             -------!R
>                            ;B|-;!B               ;B|-;!B
>                            ---------------------------------otimes-R
>    A, A-o!B;|-;!B          ;B|-;!B otimes !B
>    ------------------------------------------Cut
>    A, A-o!B;|-;!B
> 
> How does one eliminate the Cut from this proof?
> 
> This problem is closely related to one identified in the natural 
> deduction
> formulation of linear logic by Hyland et al., and also discussed in my 
> paper,
> "There's no substitute for linear logic".
> 
> Cheers,  -- P
> 
> 
> Philip Wadler, Professor of Theoretical Computer Science
> Informatics, University of Edinburgh
> JCMB, King's Buildings, Mayfield Road
> Edinburgh EH9 3JZ SCOTLAND
> +44 131 650 5174 http://homepages.inf.ed.ac.uk/wadler/