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

2019/12/08 by Pentus, Anna, Pentus, Mati
#03B47 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1912.03739

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.

Related

• Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities
• Proof nets for display logic
• Proof nets for the Lambek-Grishin calculus
• Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic
• Undecidability of the Lambek calculus with subexponential and bracket\n modalities