[Prev][Next][Index][Thread]

Question about !



I have a simple question about the two common presentations of the
rules for !. I've discussed this with several linear-logicians, without
reaching a conclusion. 

Two presentations commonly used (for single-conclusion calculi) are

(I)  !Gamma |- A        Gamma, !A, !A |- B      Gamma, A |- B      Gamma |- B
     -----------        ------------------      --------------     ------------
     !Gamma |- !A       Gamma, !A  |- B         Gamma, !A |- B    Gamma, !A |-B

and

(II) The last three rules above with the first rule replaced by:
 
        B |- I    B |- A    B |- B \otimes B   (where I is the unit of \otimes)
        ------------------------------------
                  B |- !A

System (II)  is the categorical combinator version of the rules, characterising
!A as a greatest fixed point (coinductive type).

My question is, when are the same sequents derivable in linear logic using 
presentations (I) and (II) of the rules for ! ? The answer may  differ 
depending on the fragment of linear logic we are interested in. 

Clearly rules (I) are derivable from rules (II) (using rules for the unit I
and \otimes, together with Cut and the Identity axiom).

Can anyone tell me under what circumstances the same sequents are provable
using (I) and (II)?



Thanks,
Carolyn