arXiv · 1912.03739
Proof nets for the Lambek calculus with one division and a negative-polarity modality for weakening
Abstract
In this paper, we introduce a variant of the Lambek calculus allowing empty antecedents. This variant uses two connecives: the left division and a unary modality that occurs only with negative polarity and allows weakening in antecedents of sequents. We define the notion of a proof net for this calculus, which is similar to those for the ordinary Lambek calculus and multiplicative linear logic. We prove that a sequent is derivable in the calculus under consideration if and only if there exists a proof net for it. Thus, we establish a derivability criterion for this calculus in terms of the existence of a graph with certain properties. The size of the graph is bounded by the length of the sequent.
Explore related subjects
Keep this discovery
Anna Pentus, Mati Pentus. 2019-12-08. Proof nets for the Lambek calculus with one division and a negative-polarity modality for weakening. https://arxiv.org/abs/1912.03739
Cite the original work for its findings. Save a collection to share your selection of sources.