[Prev][Next][Index][Thread]
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.
- 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
>
>
>
References: