Re: Cut-Elimination in Linear Logic
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
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.
>> I think I understand what LU fragment you're looking at
>> 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:
> 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
> 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