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

TL;DR

This paper introduces a new sequent calculus FL' for non-commutative substructural logic, exploring how associativity and distributivity influence the non-eliminability of the cut rule, and compares it with the standard FL calculus.

Contribution

It presents a novel sequent calculus FL' with specific structural rule restrictions and analyzes the impact of associativity and distributivity on cut rule eliminability.

Findings

FL' has the same proof strength as standard FL

Associativity and distributivity are linked to cut rule non-eliminability

Differences in left rule parameters affect proof construction

Abstract

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, i.e. contraction, weakening and exchange. (FL' is based on our investigations of the Gentzen-style natural deduction for non-commutative substructural logics.) FL' has the same proof strength as the standard sequent calculus FL (Full Lambek), which is the basic sequent calculus for all other substructural logics. For the standard FL, we use Ono's formulation. Although FL' and the standard FL are equivalent, there is a subtle difference in the left rule of implication. In the standard FL, two parameters $\Gamma_1$ and $\Gamma_2$(resp.), each of which is just an finite sequence of arbitrary formulas, appear on the left and right side (resp.) of a formula which is placed on the left side of the sequent on the upper left side of the left rule $\imply$ (which corresponds to $\imply'$ in FL'). On the other hand, there is no such parameter on the left side of the sequent on the upper left side in the left rule for $\imply'$ of FL'. In FL', $\Gamma_1$ is always empty, and only $\Gamma_2$ is allowed to occur in the left rule for $\imply'$. (Similar differences occur in multiplicative and additive conjunctions, and in additive disjunction.) This difference between FL' and FL matters deeply, for we are led to a construction of proof-figures in FL', which show how the associativity of multiplicative conjunction and the distributivity of multiplicative conjunction over additive disjunction are involved in the eliminations of the cut rule in those proof-figures. We specify how associativity and distributivity are related to the non-eliminability of an application of the cut rule in those proof-figures of FL'.