question from Phil Wadler re cut/linear logic

Jeremy DAWSON <jeremy@discus.anu.edu.au> · Thu, 20 Nov 2003 10:44:40 +1100 (EST)

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

> Consider the following proof

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

But how is this an instance of the Cut rule which you define as

   G;G'|-D';D,A   A,L;G'|-D';P
   ---------------------------Cut
   G,L;G'|-D';D,P

Should this be 
                           ;B|-;!B otimes !B
                           ----------------- !L
   A, A-o!B;|-;!B          !B;|-;!B otimes !B
   ------------------------------------------Cut(a)
   A, A-o!B;|-;!B otimes !B
?

Assuming so, we could obtain 

                           ;B|-;!B otimes !B
                           ----------------- !L
         !B;|-;!B          !B;|-;!B otimes !B
         ------------------------------------Cut(b)
               !B;|-;!B otimes !B
             -----------------------------(...)
             A, A-o!B;|-;!B otimes !B

where (...) represents the derivation of 
    A, A-o!B;|-;!B
which was left unspecified, and assuming that this (...)
derivation could be transformed to a derivation of 
    A, A-o!B;|-;!B otimes !B
from 
    !B;|-;!B otimes !B

>From here we see that the cut(b) is completely superfluous
since its conclusion is the same as its right premise.
Thus we can obtain 

	       ;B|-;!B otimes !B
	       ----------------- !L
               !B;|-;!B otimes !B
             -----------------------------(...)
             A, A-o!B;|-;!B otimes !B

This has now eliminated the cut as long as the moves represented 
by (...) are legal. 

Having looked at Girard's paper we cannot see how to fill in the (...)
moves for deriving 
    A, A-o!B;|-;!B

Jeremy Dawson and  Rajeev Gore 