One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity

Bilinear Logic of Lambek [10] amounts to Noncommutative MALL of Abrusci [1]. Lambek [10] proves the cut–elimination theorem for a onesided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek [10], we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTIME complexity of the multiplicative fragment of NBL.