Linearizing intuitionistic implication (Q1210141)

In the introduction the authors give a nice description of how linear logic is obtained from classical and intuitionistic logic by a modification in three steps. IIL denotes Implicational propositional Intuitionistic Logic. And IMALL is the Intuitionistic fragment of Multiplicative-Additive Linear Logic. Contrary to IIL, IMALL has neither contraction nor weakening and expressly forbids the copying of the principal formula of any rule into a premise. IIL* results from IIL by modifying one of its rules and by discarding the cut and contraction rules. The advantage of IIL* is that there is no copying of principal formulas. Lemmas 3.2 and 3.4 state that given a proof of \(\Gamma\vdash C\) in IIL, a proof of \(\Gamma\vdash C\) can be constructed in ILL*, and, conversely, given a proof of \(\Gamma\vdash C\) in IIL*, a proof of \(\Gamma\vdash C\) can be constructed in IIL. The lack of contraction in IIL* makes the formulation of the sequent rules for implicational intuitionistic propositional logic amenable to encoding into IMALL. For any IIL* sequent \(\Gamma\vdash C\) let \(\theta(\Gamma\vdash C)\) be its translation into IMALL. The authors show in section 5 that there exists a cut-free proof of \(\Gamma\vdash C\) in IIL* if and only if there is a cut- free proof of \(\theta(\Gamma\vdash C)\) in IMALL. This establishes their Theorem 1.1: IIL can be embedded into IMALL. The embedding preserves the structure of cut-free proofs in IIL*. In section 6 the authors show that the embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL.