Abstract:
In Lafont's soft linear logic the rule of contraction is replaced by the
so-called rule of multiplexing. Here we consider a version of
multiplexing where !A implies any positive number of copies of A. The
weakening rule is not allowed. We also borrow the ! introduction rule
from Girard's light linear logic. Here we study Lambek calculus enriched
with these rules. We prove that Lambek calculus so enriched satisfies
cut elimination, substitution, and Lambek’s non-emptiness restriction,
that is, the left-hand side of any provable sequent is non-empty. We
show that this calculus is undecidable. If a number of copies of A in
the multiplexing rule is bounded by a fixed constant, then the calculus
becomes decidable.
