Journal of Symbolic Logic 59 (2):419-444 (1994)
AbstractWe study interpolation for elementary fragments of classical linear logic. Unlike in intuitionistic logic (see [Renardel de Lavalette, 1989]) there are fragments in linear logic for which interpolation does not hold. We prove interpolation for a lot of fragments and refute it for the multiplicative fragment (→, +), using proof nets and quantum graphs. We give a separate proof for the fragment with implication and product, but without the structural rule of permutation. This is nearly the Lambek calculus. There is an appendix explaining what quantum graphs are and how they relate to proof nets
Similar books and articles
Interpolation and Amalgamation Properties in Varieties of Equivalential Algebras.Małgorzata Porębska - 1986 - Studia Logica 45 (1):35 - 38.
Interpolation and Definability in Guarded Fragments.Eva Hoogland & Maarten Marx - 2002 - Studia Logica 70 (3):373 - 409.
Interpolation in Fragments of Intuitionistic Propositional Logic.Gerard R. Renardel de Lavalette - 1989 - Journal of Symbolic Logic 54 (4):1419-1430.
A New Correctness Criterion for the Proof Nets of Non-Commutative Multiplicative Linear Logics.Misao Nagayama & Mitsuhiro Okada - 2001 - Journal of Symbolic Logic 66 (4):1524-1542.
The Conjoinability Relation in Lambek Calculus and Linear Logic.Mati Pentus - 1994 - Journal of Logic, Language and Information 3 (2):121-140.
A New Correctness Criterion for Cyclic Proof Nets.V. Michele Abrusci & Elena Maringelli - 1998 - Journal of Logic, Language and Information 7 (4):449-459.
Interpolation in Fragments of Intuitionistic Propositional Logic.Gerard R. Renardel De Lavalette - 1989 - Journal of Symbolic Logic 54 (4):1419 - 1430.
Added to PP
Historical graph of downloads