[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