Hostname: page-component-8448b6f56d-tj2md Total loading time: 0 Render date: 2024-04-23T10:12:30.267Z Has data issue: false hasContentIssue false
  • English
  • Français

Interpolation in fragments of classical linear logic

Published online by Cambridge University Press:  12 March 2014

Dirk Roorda
Dirk Roorda*
Affiliation:
Department of Computer Science, Rijksuniversiteit Groningen, 9747 AC Groningen, The Netherlands
Get access Rights & Permissions [Opens in a new window]

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.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 59 , Issue 2 , June 1994 , pp. 419 - 444
Copyright
Copyright © Association for Symbolic Logic 1994

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Danos, V. and Regnier, L. [1989], The structure of multiplicatives, Archive for Mathematical Logic, vol. 28, pp. 181–203.Google Scholar
Girard, J-Y. [1987], Theoretical Computer Science, vol. 50, pp. 1–102.Google Scholar
de Lavalette, G. R. Renardel [1989], this JOURNAL, vol. 54, pp. 1419–1430.Google Scholar
Roorda, D. [1991a], Chapter III of [Roorda, 1991d]; this has appeared as [Roorda, 1992].Google Scholar
Roorda, D. [1991b], Chapter IV of [Roorda, 1991d]; this has appeared in [Roorda, 1991c].Google Scholar
Roorda, D. [1991c], Lambek calculus: Proof-theoretical investigations, Technical report, Centre for Cognitive Science, University of Edinburgh, 2 Buccleuch Place, Edinburgh EHS 9LW, UK, Part of Deliverable R1.2.F. ESPRIT Basic research action DYANA BR3175.Google Scholar
Roorda, D. [1991d], Resource Logics: proof-theoretical investigations, Ph.D. thesis, Fac. Math, and Comp. Sc., University of Amsterdam, Amsterdam.Google Scholar
Roorda, D. [1992], Proof nets for Lambek calculus, Journal of Logic and Computation, vol. 2, pp. 211–231.Google Scholar
Schütte, K. [1962], Der Interpolitionssatz der intuitionistischen Prädikatenlogik, Mathematische Annalen, vol. 148, pp. 192–200.Google Scholar