Cut-Elimination in Linear Logic

[sanjiva at cse.iitd.ernet.in]

The out rules on +ve (L) and -ve (R) do not increase increase
the class of *equivalent Linear Logic sequents* provable, but
provide (as you noted) nicer encodings for various conectives
(chimeric, Girard calls them), with nice properties -- you've
noted associativity -- arising from idempotence of ! or ? etc.
The  semantics  is consequently nicer, and more in line with the
requirements you've noted in some of your earlier papers.

- S.


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