On non-eliminability of the cut rule and the roles of associativity and distributivity in non-commutative substructural logics

Takeshi Ueno, Koji Nakaogawa, Osamu Watari

We introduce a sequent calculus FL' for non-commutative substructural logic. It has at most one formula on the right side of sequent, and excludes three structural inference rules,…