Исчисление Ламбека, обогащенное субэкспоненциалами

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.