Linearizing intuitionistic implication
type: Item
instance of: scholarly article
title: Linearizing intuitionistic implication
zbMATH Open document ID: 0767.03006
DOI: 10.1016/0168-0072(93)90041-B
author: Natarajan Shankar
author: P. Lincoln
author: Andre Scedrov
published in: Annals of Pure and Applied Logic
publication date: 1993-05-16T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 169667
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: linear logic
zbMATH Keywords: cut-free proof
describes a project that uses: Lolli
MaRDI profile type: Publication
cites work: Computational interpretations of linear logic
cites work: Logic Programming with Focusing Proofs in Linear Logic
cites work: Q3357521
cites work: Accessible categories and models of linear logic
cites work: A game semantics for linear logic
cites work: Q5547552
cites work: Contraction-free sequent calculi for intuitionistic logic
cites work: Linear logic
cites work: Q4204146
cites work: Q3791120
cites work: Q3994895
cites work: Bounded linear logic: A modular approach to polynomial-time computability
cites work: Q5812175
cites work: The linear abstract machine
cites work: Decision problems for propositional linear logic
cites work: Q3997125
cites work: Uniform proofs as a foundation for logic programming
cites work: Q3972527
cites work: Q5519124
cites work: Intuitionistic propositional logic is polynomial-space complete
cites work: Q3259711
cites work: Q5771193
description: scientific article; zbMATH DE number 169667