Unit-free ordered Lambek calculus

The calculus ${\mathcal{L}}_{\mathrm{ord}}$ of chapter 38 has atoms, ordered possibly empty context words, one succedent, binary product, and both residuals. Context concatenation is associative at the metalevel. There is no product unit, additive, modality, weakening, contraction, exchange, or formula equation for associativity.

Ordered single-cut admissibility is theorem 38.6; ordered simultaneous substitution is corollary 38.7; cut elimination is theorem 38.8; and both residuation equivalences are theorem 38.9. Strict weight descent gives the terminating, sound, and complete cut-free decision procedure of theorem 38.13.

Distinct atoms witness noncommutativity at product. The separately named calculus ${\mathcal{L}}_{\mathrm{ex}}$ adds one explicit adjacent-exchange rule. Planar drawings, braid equations, and the symmetric double-crossing equation are compared but are not additional metatheorems of ${\mathcal{L}}_{\mathrm{ord}}$.

Lambek 1958 is the historical source and requires nonempty antecedents. Veltri treats ordered, possibly empty contexts and a richer natural-deduction language with multiplicative unit. The unit-free sequent cut-elimination and search proofs used here are local; no result about Lambek–Grishin logic is imported.

The pinned Kappa corpus implements the finite syntax-directed proof search as object-language data. Its appendix E entry checks positive, negative, residuation, product, and word-order cases. It is implementation evidence, not a mechanized proof of cut elimination, search exactness, or complexity.