  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.
