INCLUSION CRITERIA
An entry belongs in this subdivision if and only if its consequence relation omits the exchange rule, so that hypotheses form an ordered (non-commutative) structure and implication is directional.
Required: At least one of the following:
- A sequent calculus without exchange, in which antecedent order is fixed
- Directed implications (\, /) residuating a non-commutative product
- A displacement or discontinuity operation over ordered contexts
Not sufficient: Dropping weakening or contraction while keeping exchange (Linear, Affine, Relevant). A commutative substructural base.
Boundary: The Lambek family is applied to natural-language syntax; its use as categorial/type-logical grammar is cross-listed with Applications/Semantics and Type. The pure order-sensitive proof theory belongs here.