Some Syntactical Observations on Linear Logic
Harold Schellinx · Journal of Logic and Computation · 1991
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 into classical linear logic (CLL) and characterize intutionstic linear logic (ILL) as the logic obtained from CLL by imposing a restriction on the right-rule for linear implication while keeping the property of Cut elimination. Also it is shown that CLL is not conservative over ILL.