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

TL;DR

This paper introduces a variant of the Lambek calculus with a negative-polarity modality for weakening, providing a proof net characterization that offers a graph-based derivability criterion.

Contribution

It extends the Lambek calculus with a negative-polarity modality and proof nets, establishing a new derivability criterion based on graph properties.

Findings

Proof nets characterize derivability in the new calculus.

The proof net size is bounded by the sequent length.

The calculus allows empty antecedents with 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.