Interpolation in fragments of classical linear logic

1994 ◽  
Vol 59 (2) ◽  
pp. 419-444 ◽  
Author(s):  
Dirk Roorda
Keyword(s):  
Intuitionistic Logic ◽  
Linear Logic ◽  
Quantum Graphs ◽  
Lambek Calculus ◽  
Structural Rule ◽  
Proof Nets

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.

scholarly journals Proof nets for multiplicative cyclic linear logic and Lambek calculus

2019 ◽  
Vol 29 (06) ◽  
pp. 733-762
Author(s):  
V. Michele Abrusci ◽  
Roberto Maieli
Keyword(s):  
Linear Logic ◽  
Lambek Calculus ◽  
Correctness Criterion ◽  
Proof Nets ◽  
Technical Achievement ◽  
Cyclic Fragment

AbstractThis paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic LL. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non-inductive) way to parse phrases or sentences by means of Lambek proof nets.

scholarly journals Proof nets and semi-star-autonomous categories

2014 ◽  
Vol 26 (5) ◽  
pp. 789-828 ◽  
Author(s):  
WILLEM HEIJLTJES ◽  
LUTZ STRAßBURGER
Keyword(s):  
Linear Logic ◽  
Proof Nets

In this paper, it is proved that Girard's proof nets for multiplicative linear logic characterize free semi-star-autonomous categories.

The finite model property for knotted extensions of propositional linear logic

2005 ◽  
Vol 70 (1) ◽  
pp. 84-98 ◽  
Author(s):  
C. J. van Alten
Keyword(s):  
Linear Logic ◽  
Finite Model ◽  
Algebraic Semantics ◽  
Structural Rule ◽  
Model Property ◽  
Algebraic Models ◽  
Finite Model Property ◽  
Finite Embeddability Property ◽  
Full Algebra ◽  
Intuitionistic Linear Logic

AbstractThe logics considered here are the propositional Linear Logic and propositional Intuitionistic Linear Logic extended by a knotted structural rule: . It is proved that the class of algebraic models for such a logic has the finite embeddability property, meaning that every finite partial subalgebra of an algebra in the class can be embedded into a finite full algebra in the class. It follows that each such logic has the finite model property with respect to its algebraic semantics and hence that the logic is decidable.

scholarly journals Subformula Linking for Intuitionistic Logic with Application to Type Theory

2021 ◽  
pp. 200-216
Author(s):  
Kaustuv Chaudhuri
Keyword(s):  
Theorem Proving ◽  
Intuitionistic Logic ◽  
Type Theory ◽  
Linear Logic ◽  
Interactive Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
Direct Manipulation ◽  
First Order

AbstractSubformula linking is an interactive theorem proving technique that was initially proposed for (classical) linear logic. It is based on truth and context preserving rewrites of a conjecture that are triggered by a user indicating links between subformulas, which can be done by direct manipulation, without the need of tactics or proof languages. The system guarantees that a true conjecture can always be rewritten to a known, usually trivial, theorem. In this work, we extend subformula linking to intuitionistic first-order logic with simply typed lambda-terms as the term language of this logic. We then use a well known embedding of intuitionistic type theory into this logic to demonstrate one way to extend linking to type theory.

scholarly journals Reconciling Lambek’s restriction, cut-elimination and substitution in the presence of exponential modalities

2020 ◽  
Vol 30 (1) ◽  
pp. 239-256 ◽  
Author(s):  
Max Kanovich ◽  
Stepan Kuznetsov ◽  
Andre Scedrov
Keyword(s):  
Linear Logic ◽  
Cut Elimination ◽  
Lambek Calculus ◽  
Full Extent ◽  
Intuitionistic Linear Logic

Abstract The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. Interestingly enough, we show that for any system equipped with a reasonable exponential modality the following holds: if the system enjoys cut elimination and substitution to the full extent, then the system necessarily violates Lambek’s restriction. Nevertheless, we show that two of the three conditions can be implemented. Namely, we design a system with Lambek’s restriction and cut elimination and another system with Lambek’s restriction and substitution. For both calculi, we prove that they are undecidable, even if we take only one of the two divisions provided by the Lambek calculus. The system with cut elimination and substitution and without Lambek’s restriction is folklore and known to be undecidable.

scholarly journals Preface

2016 ◽  
Vol 28 (7) ◽  
pp. 991-994
Author(s):  
LORENZO TORTORA DE FALCO
Keyword(s):  
Taylor Expansion ◽  
Linear Logic ◽  
Research Area ◽  
Theoretical Computer Science ◽  
Quantitative Approach ◽  
Algebraic Setting ◽  
Use Of Resources ◽  
Natural Notion ◽  
Proof Nets ◽  
New Ideas

This special issue is devoted to some aspects of the new ideas that recently arose from the work of Thomas Ehrhard on the models of linear logic (LL) and of the λ-calculus. In some sense, the very origin of these ideas dates back to the introduction of LL in the 80s by Jean-Yves Girard. An obvious remark is that LL yielded a first logical quantitative account of the use of resources: the logical distinction between linear and non-linear formulas through the introduction of the exponential connectives. As explicitly mentioned by Girard in his first paper on the subject, the quantitative approach, to which he refers as ‘quantitative semantics,’ had a crucial influence on the birth of LL. And even though, at that time, it was given up for lack of ‘any logical justification’ (quoting the author), it contained rough versions of many concepts that were better understood, precisely introduced and developed much later, like differentiation and Taylor expansion for proofs. Around 2003, and thanks to the developments of LL and of the whole research area between logic and theoretical computer science, Ehrhard could come back to these fundamental intuitions and introduce the structure of finiteness space, allowing to reformulate this quantitative approach in a standard algebraic setting. The interpretation of LL in the category Fin of finiteness spaces and finitary relations suggested to Ehrhard and Regnier the differential extensions of LL and of the simply typed λ-calculus: Differential Linear Logic (DiLL) and the differential λ-calculus. The theory of LL proof-nets could be straightforwardly extended to DiLL, and a very natural notion of Taylor expansion of a proof-net (and of a λ-term) was introduced: an element of the Taylor expansion of the proof-net/term α is itself a (differential) proof-net/term and an approximation of α.

Sign in / Sign up

Export Citation Format

Share Document