The unit-free ordered Lambek calculus

The formulas, context words, and sequents of chapter 38 are $$A,B::=p\mid A\cdot B\mid A\mathrm{\backslash }B\mid B/A,\mathrm{\Gamma }::=ϵ\mid A,\mathrm{\Gamma },\mathrm{\Gamma }\Rightarrow A.$$ Greek capital metavariables denote possibly empty ordered contexts. The language has no formula for the empty-context unit. Context equality never exchanges adjacent formulas. The complete cut-free rule set is

$A\Rightarrow A$

$\mathrm{\Gamma }\Rightarrow A$$\mathrm{\Delta }\Rightarrow B$

$\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow A\cdot B$

$\mathrm{\Delta },A,B,\mathrm{\Theta }\Rightarrow C$

$\mathrm{\Delta },A\cdot B,\mathrm{\Theta }\Rightarrow C$

$A,\mathrm{\Gamma }\Rightarrow B$

$\mathrm{\Gamma }\Rightarrow A\mathrm{\backslash }B$

$\mathrm{\Gamma }\Rightarrow A$$\mathrm{\Delta },B,\mathrm{\Theta }\Rightarrow C$

$\mathrm{\Delta },\mathrm{\Gamma },A\mathrm{\backslash }B,\mathrm{\Theta }\Rightarrow C$

$\mathrm{\Gamma },A\Rightarrow B$

$\mathrm{\Gamma }\Rightarrow B/A$

$\mathrm{\Gamma }\Rightarrow A$$\mathrm{\Delta },B,\mathrm{\Theta }\Rightarrow C$

$\mathrm{\Delta },B/A,\mathrm{\Gamma },\mathrm{\Theta }\Rightarrow C$

Cut is not a primitive rule. Its admissible ordered form is $$\frac{\begin{array}{c}\mathrm{\Gamma }\Rightarrow A\\ \mathrm{\Delta },A,\mathrm{\Theta }\Rightarrow C\end{array}}{\mathrm{\Delta },\mathrm{\Gamma },\mathrm{\Theta }\Rightarrow C}\mathrm{Cut}.$$ Backward proof search tries Id, then the applicable succedent rule, then scans antecedent occurrences from left to right. At a product it tries Prod-L. At $A\mathrm{\backslash }B$ it enumerates the prefix as $\mathrm{\Delta },\mathrm{\Gamma }$ by increasing $|\mathrm{\Delta }|$; at $B/A$ it enumerates the suffix as $\mathrm{\Gamma },\mathrm{\Theta }$ by increasing $|\mathrm{\Gamma }|$. The traversal is depth first.

The only structural extension used in the chapter adds $$\frac{\mathrm{\Delta },A,B,\mathrm{\Theta }\Rightarrow C}{\mathrm{\Delta },B,A,\mathrm{\Theta }\Rightarrow C}\mathrm{Ex}.$$ No braid or symmetry equation is part of either displayed calculus.