Sequent systems for compact bilinear logic

Compact Bilinear Logic (CBL), introduced by Lambek 14], arises from the multiplicative fragment of Noncommutative Linear Logic of Abrusci 1] (also called Bilinear Logic in 13]) by identifying times with par and 0 with 1. In this paper, we present two sequent systems for CBL and prove the cut‐elimination theorem for them. We also discuss a connection between cut‐elimination for CBL and the Switching Lemma from 14].