Interpolation in fragments of classical linear logic
Copyright policy )Interpolation in fragments of classical linear logic
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.
- University of Groningen Netherlands
- Royal Netherlands Academy of Arts and Sciences (KNAW) Netherlands
Proof theory in general (including proof-theoretic semantics), fragments, interpolation theorem, propositional linear logic, Subsystems of classical logic (including intuitionistic logic)
Proof theory in general (including proof-theoretic semantics), fragments, interpolation theorem, propositional linear logic, Subsystems of classical logic (including intuitionistic logic)
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).7 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!