# Cut-Elimination in Linear Logic

Fri Nov 21 10:11:03 EST 2003

```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

```