The purpose of this note is to clarify some syntactical matters in linear logic. We present a detailed proof of the faithfulness of Girard's embedding of intutionitic logic intoclassicallinear logic (CLL) and characterizeintutionsticlinear logic (ILL) as the logic obtained fromCLLby imposing a restriction on the right-rule for linear implication while keeping the property of Cut elimination. Also it is shown thatCLLis not conservative overILL.
展开▼
