Proof nets for the Lambek calculus with one division and a negative-polarity modality for weakening

DOI10.1007/S10958-022-05853-5arXiv1912.03739WikidataQ114017517 ScholiaQ114017517MaRDI QIDQ6330702FDOQ6330702

Authors: A. E. Pentus, Mati Pentus Edit this on Wikidata

Publication date: 8 December 2019

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.

Mathematics Subject Classification ID

Proof theory and constructive mathematics (03Fxx) Theory of computing (68Qxx) General logic (03Bxx)

This page was built for publication: Proof nets for the Lambek calculus with one division and a negative-polarity modality for weakening

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6330702)