Interpolation in Fragments of Classical Linear Logic

Dirk Roorda

doi:10.2307/2275398

Interpolation in Fragments of Classical Linear Logic

Dirk Roorda

DANS-KNAW

Research output: Contribution to journal/periodical › Article › Scientific › peer-review

Abstract

We 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.

Original language	English
Pages (from-to)	419
Number of pages	25
Journal	Journal of Symbolic Logic
Volume	59
Issue number	2
DOIs	https://doi.org/10.2307/2275398
Publication status	Published - 1994

Access to Document

10.2307/2275398Licence: CC BY

Cite this

@article{83b95afe96b546aa88eb46da6310aff9,

title = "Interpolation in Fragments of Classical Linear Logic",

abstract = "We 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.",

author = "Dirk Roorda",

year = "1994",

doi = "10.2307/2275398",

language = "English",

volume = "59",

pages = "419",

journal = "Journal of Symbolic Logic",

issn = "0022-4812",

publisher = "Association for Symbolic Logic",

number = "2",

}

TY - JOUR

T1 - Interpolation in Fragments of Classical Linear Logic

AU - Roorda, Dirk

PY - 1994

Y1 - 1994

N2 - We 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.

AB - We 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.

U2 - 10.2307/2275398

DO - 10.2307/2275398

M3 - Article

SN - 0022-4812

VL - 59

SP - 419

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

IS - 2

ER -

Interpolation in Fragments of Classical Linear Logic

Abstract

Access to Document

Fingerprint

Cite this