Ordered and Noncommutative Types and the Lambek Calculus
Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.
Linear use does not determine order. In the linear calculus of chapter 18, exchange is built into equality of contexts. Thus a resource may be used once and nevertheless pass another resource on its way to the consumer. For a word, a protocol message, or a stack action, that crossing can be the error we need the type system to reject.
Take distinct atoms 𝑝 and 𝑞. Product introduction ought to derive 𝑝,𝑞⇒𝑝⋅𝑞. It must not derive 𝑞,𝑝⇒𝑝⋅𝑞: both assumptions occur exactly once, but in the wrong order. We therefore replace contexts-as-maps by context words. Product combines adjacent resources; its two residuals solve for a missing factor on the left or right. The same order discipline models a tiny stack protocol: if 𝑝 means “a value has just been pushed” and 𝑝\𝑞 is an action that must consume that value on its left before producing state 𝑞, then 𝑝,𝑝\𝑞⇒𝑞 is derivable while the reversed schedule is not. Protocol messages have the same shape when a response must follow its request.
The notation is the ordered version of the resource connectives in chapter 18: product 𝐴⋅𝐵 plays the role of a noncommutative tensor; 𝐴\𝐵 and 𝐵/𝐴 are the left and right ordered implications. If exchange were restored, the two residuals would become interderivable and recover the one-sided behavior of linear implication 𝐴⊸𝐵, as proved in proposition 38.17. Here the side on which the argument arrives remains part of the formula.
The calculus Lord is the unit-free, intuitionistic Lambek sequent calculus with possibly empty antecedents. It has atoms, product, and both residuals. Concatenation of contexts is associative at the metalevel; product remains a binary formula former. Unlike Lambek’s original calculus, Lord admits the empty antecedent [Lam58].
Contexts are words
Let 𝜖 be the empty word. An ordered context is a finite word of formulas. If Γ and Δ are ordered contexts, then Γ,Δ is their concatenation. There is no equation Γ,𝐴,𝐵,Δ=Γ,𝐵,𝐴,Δ. Thus contexts form the free monoid on formulas: 𝜖 is the identity, concatenation is associative, and no commutativity equation is imposed. One may picture a context as a row of matrices whose multiplication order cannot be reversed; the analogy concerns order only, not matrix semantics.
Fix a set of atoms 𝖠𝗍. Formulas and contexts are generated by 𝐴,𝐵::=𝑝∣𝐴⋅𝐵∣𝐴\𝐵∣𝐵/𝐴,Γ::=𝜖∣𝐴,Γ,𝑝∈𝖠𝗍. A sequentΓ⇒𝐴 has one ordered input word and one output. The arrow ⇒ is punctuation separating antecedent from succedent; it is not a formula connective. Greek capitals Γ,Δ,Θ denote context words, while Roman capitals 𝐴,𝐵,𝐶,𝑋,𝑌 denote single formulas. Each of them is a word, never the finite-map linear context of chapter 18. The complete ordered rule sheet is collected in subappendix A.52. The connective 𝐴\𝐵 waits for an 𝐴 on its left; 𝐵/𝐴 waits for an 𝐴 on its right. Here \ is always a formula connective, unrelated to the row-lacks predicate of chapter 4. For invertible square matrices the positional mnemonic is literal: 𝐴\𝐵⇝𝐴−1𝐵,𝐵/𝐴⇝𝐵𝐴−1. Lambek residuals are order-theoretic adjoints, not matrix inverses, but the two formulas differ for exactly the same reason that multiplication order matters.
The rules must expose every context split. In the two left-residual rules, the premise deriving 𝐴 is inserted on the side from which the residual expects 𝐴.
Derivations are generated by the following seven rules. Every metavariable written with a Greek capital letter denotes an ordered context, possibly empty; 𝐴,𝐵,𝐶,𝑋,𝑌 denote formulas.
Identity and the product rules give the expansion 𝑋𝐴⇒𝐴Id𝑋𝐵⇒𝐵Id𝐴,𝐵⇒𝐴⋅𝐵Prod−R𝐴⋅𝐵⇒𝐴⋅𝐵Prod−L. Rule Bslash-L places the argument immediately to the left of its residual: 𝑋𝐴⇒𝐴Id𝑋𝐵⇒𝐵Id𝐴,𝐴\𝐵⇒𝐵Bslash−L. Rule Slash-L places the argument immediately to the right: 𝑋𝐴⇒𝐴Id𝑋𝐵⇒𝐵Id𝐵/𝐴,𝐴⇒𝐵Slash−L. Rule Slash-R abstracts the rightmost argument: 𝐴⇒𝐴𝐵⇒𝐵𝐴,𝐴\𝐵⇒𝐵Bslash−L𝐴⇒𝐵/(𝐴\𝐵)Slash−R. Rule Bslash-R abstracts the leftmost argument: 𝐴⇒𝐴𝐵⇒𝐵𝐵/𝐴,𝐴⇒𝐵Slash−L𝐴⇒(𝐵/𝐴)\𝐵Bslash−R. Every application tree preserves the left-to-right order of its premises; no exchange step occurs.
★★☆ Construct cut-free derivations of (𝐴⋅𝐵)⋅𝐶⇒𝐴⋅(𝐵⋅𝐶)and𝐴⋅(𝐵⋅𝐶)⇒(𝐴⋅𝐵)⋅𝐶. Mark every split used by Prod-R. Do not appeal to a formula equation between the two products.
Proof. The reverse implication is Id. For the forward implication, inspect the last rule. No left rule applies because the antecedent has no compound formula. No right rule applies because the succedent is atomic. The last rule is therefore Id, whose conclusion is exactly 𝑝⇒𝑝. ◻
Proof. With atomic antecedents and a product succedent, the last rule can only be Prod-R. A split of the two-letter word 𝑞,𝑝 must make one premise derive 𝑝 and the other derive 𝑞. The three splits are 𝜖∣𝑞,𝑝,𝑞∣𝑝,𝑞,𝑝∣𝜖. The outer splits require an atomic conclusion from an empty context. The middle split requires 𝑞⇒𝑝 and 𝑝⇒𝑞. Every case contradicts lemma 38.3. With exchange, first derive 𝑝,𝑞⇒𝑝⋅𝑞 by two identities and Prod-R, then apply Ex. ◻
★★☆ Let 𝑝,𝑞,𝑟 be distinct atoms. For each of the six permutations 𝜋 of 𝑝,𝑞,𝑟, decide whether 𝜋(𝑝,𝑞,𝑟)⇒𝑝⋅(𝑞⋅𝑟) is derivable. For every negative answer, give the failed final split and invoke lemma 38.3.
The proposed ordered cut replaces one marked formula occurrence by the ordered context that derives it: Γ⇒𝐴Δ,𝐴,Θ⇒𝐶Δ,Γ,Θ⇒𝐶Cut. The height ℎ(D) is the number of rule occurrences on a longest branch. Define |𝑝|=1,|𝑋∘𝑌|=|𝑋|+|𝑌|+1(∘∈{⋅,\,/}). The rank of one cut is the lexicographically ordered pair (|𝐴|,ℎ(D)+ℎ(E)). The antecedent occurrence cut from E is regarded as marked; this distinguishes it from other occurrences of the same formula.
If Cut were admitted during backward search, even an atomic goal would have one candidate for every formula 𝐴: Γ⇒𝐴Δ,𝐴,Θ⇒𝑝Δ,Γ,Θ⇒𝑝𝐶𝑢𝑡(𝐴=𝑝,𝑝⋅𝑝,𝑝\𝑝,…). A naive search node therefore has unbounded branching. Cut admissibility removes that choice and recovers the subformula-bounded search below.
Proof of Theorem 38.6 — Ordered single-cut admissibility
Proof. Induct on the rank in definition 38.5. Commute a nonprincipal cut upward, erase identity cuts, and replace a principal cut by cuts on proper subformulas. Each transformation decreases the lexicographic rank.
Nonprincipal in the right derivation. Suppose the marked 𝐴 is not principal in the last rule 𝑅 of E. It occurs in exactly one premise. Cut D into that premise and reapply 𝑅. The possibilities are exhaustive:
last rule of E
premise containing the marked occurrence
Prod-R
left premise or right premise
Prod-L
its unique premise
Bslash-R, Slash-R
their unique premise
Bslash-L, Slash-L
argument premise or continuation premise
For example, if the marked occurrence is in the left premise of Prod-R, the reduction is D:Γ⇒𝐴E1:Δ,𝐴,Θ⇒𝑋E2:Σ⇒𝑌Δ,𝐴,Θ,Σ⇒𝑋⋅𝑌Prod−RΔ,Γ,Θ,Σ⇒𝑋⋅𝑌Cut. It reduces to cut(D,E1):Δ,Γ,Θ⇒𝑋E2:Σ⇒𝑌Δ,Γ,Θ,Σ⇒𝑋⋅𝑌Prod−R. For the right-premise case, perform the same reduction with the second premise in place of the first; the entire context word of the untouched first premise stays to the left of the recursive premise. For a residual-right rule, its added formula stays at the same end of the recursive premise. For a residual-left rule, recursing in the argument premise replaces precisely the contiguous block on the expected side of the residual; recursing in the continuation leaves that argument block fixed. Thus each row in the table preserves the conclusion word. The formula size is unchanged and the height of E decreases. This closes all commutes through the right derivation.
Two further commuting shapes make those placements explicit. Across Slash-R, D:Γ⇒𝐴E0:Δ,𝐴,Θ,𝑋⇒𝑌Δ,𝐴,Θ⇒𝑌/𝑋Slash−RΔ,Γ,Θ⇒𝑌/𝑋Cut. It commutes to cut(D,E0):Δ,Γ,Θ,𝑋⇒𝑌Δ,Γ,Θ⇒𝑌/𝑋Slash−R. When the marked occurrence lies inside the argument premise of Bslash-L, D:Γ⇒𝐴E1:Σ,𝐴,Π⇒𝑋E2:Δ,𝑌,Θ⇒𝐶Δ,Σ,𝐴,Π,𝑋\𝑌,Θ⇒𝐶Bslash−LΔ,Σ,Γ,Π,𝑋\𝑌,Θ⇒𝐶Cut commutes to the same Bslash-L tree with first premise cut(D,E1):Σ,Γ,Π⇒𝑋. Neither conversion crosses the residual.
It remains to handle a last rule of E whose principal formula is the marked 𝐴.
Nonprincipal in the left derivation. If the last rule of D is a left rule, the succedent 𝐴 is carried by that rule’s continuation premise. Cut that smaller premise into E, then reapply the left rule. For Bslash-L the complete schema is D1:Λ⇒𝑋D2:Π,𝑌,Ω⇒𝐴Π,Λ,𝑋\𝑌,Ω⇒𝐴Bslash−LE:Δ,𝐴,Θ⇒𝐶Δ,Π,Λ,𝑋\𝑌,Ω,Θ⇒𝐶Cut. It reduces to D1:Λ⇒𝑋cut(D2,E):Δ,Π,𝑌,Ω,Θ⇒𝐶Δ,Π,Λ,𝑋\𝑌,Ω,Θ⇒𝐶Bslash−L. The Slash-L schema places 𝑋/𝑌 before its argument block; Prod-L has only its continuation premise. Thus Bslash-L, Slash-L, and Prod-L exhaust the possible nonprincipal last rules of D, and each decreases ℎ(D). In every nonprincipal case, the recursive cut has the same cut formula, a strictly smaller input height, and the same left-to-right order of the context word.
Principal identity. If either derivation ends in the identity that is principal for the cut, erase the cut: cutting 𝐴⇒𝐴 on the left returns E, and cutting into the identity 𝐴⇒𝐴 returns D. Thus either principal identity eliminates the cut without a recursive call.
Principal product and residuals. The principal connective cases are product, backslash, and slash. For each, the following premises determine a derivation of the stated contractum.
For 𝐴=𝑋⋅𝑌, a Prod-R/Prod-L pair reduces as D1:Γ1⇒𝑋,D2:Γ2⇒𝑌,E0:Δ,𝑋,𝑌,Θ⇒𝐶,cut(D1,cut(D2,E0)):Δ,Γ1,Γ2,Θ⇒𝐶. The inner cut replaces 𝑌; the outer cut then replaces 𝑋. Their cut formulas are proper subformulas of 𝐴.
For 𝐴=𝑋\𝑌, the final rules have premises D0:𝑋,Γ⇒𝑌,E1:Σ⇒𝑋,E2:Δ,𝑌,Θ⇒𝐶. First cut E1 for the initial 𝑋 in D0, obtaining Σ,Γ⇒𝑌. Cut that result for 𝑌 in E2. The conclusion is Δ,Σ,Γ,Θ⇒𝐶, exactly the word obtained by replacing the principal occurrence in Δ,Σ,𝑋\𝑌,Θ. Both new cuts have smaller formula.
For 𝐴=𝑌/𝑋, use the premises D0:Γ,𝑋⇒𝑌,E1:Σ⇒𝑋,E2:Δ,𝑌,Θ⇒𝐶. Cut E1 for the final 𝑋 of D0, giving Γ,Σ⇒𝑌, and then cut this for 𝑌 in E2. The result is Δ,Γ,Σ,Θ⇒𝐶, matching the order in the Slash-L conclusion. Again both formulas are smaller.
Every recursive call therefore decreases the lexicographic rank. The cases are principal identity; nonprincipal Prod-L, Bslash-L, or Slash-L; and principal product, backslash, or slash, so the induction is well founded and exhaustive. ◻
The product principal case can be read as the complete tree rewrite D1:Γ1⇒𝑋D2:Γ2⇒𝑌Γ1,Γ2⇒𝑋⋅𝑌Prod−RE0:Δ,𝑋,𝑌,Θ⇒𝐶Δ,𝑋⋅𝑌,Θ⇒𝐶Prod−LΔ,Γ1,Γ2,Θ⇒𝐶Cut⇝0cut(D1,cut(D2,E0)). Both recursive cuts have a proper subformula of 𝑋⋅𝑌 as cut formula. The inner cut replaces 𝑌 first; that order is what leaves Γ1,Γ2 rather than its reversal.
A concrete instance uses two identities to introduce 𝑝⋅𝑞, then immediately eliminates that product: Put 𝐷=𝑝⇒𝑝𝑞⇒𝑞𝑝,𝑞⇒𝑝⋅𝑞Prod−R,𝐸=𝑝,𝑞⇒𝑝⋅𝑞𝑝⋅𝑞⇒𝑝⋅𝑞Prod−L. Then the complete principal reduction is 𝐷𝐸𝑝,𝑞⇒𝑝⋅𝑞Cut⇝0𝐷. This is the schematic principal rewrite above with real atoms and identity premises; no exchange or hidden proof term is involved.
The single cut is enough to substitute an entire ordered environment.
Proof of Corollary 38.7 — Ordered simultaneous substitution
Proof. Starting with D, use ordered single-cut admissibility on the marked occurrences 𝐴𝑛,𝐴𝑛−1,…,𝐴1, in that order. After replacing 𝐴𝑖, the block Ξ𝑖 occupies the same position and later cuts do not cross it. The final context is therefore the displayed concatenation. When 𝑛=0, no cut is performed and the original derivation is returned. For distinct atomic blocks, exchanging adjacent Ξ𝑖 would specialize to the underivable sequent of proposition 38.4, so the printed order is essential. ◻
Every derivation formed from the rules of definition 38.2 and finitely many uses of Cut can be transformed into a cut-free derivation of the same sequent.
Proof. Induct on the derivation. If its last rule is a logical rule with premises D𝑖, the induction hypotheses give cut-free derivations of the same premise sequents, and reapplying that rule gives the original conclusion. Identity is already cut free. If the last rule cuts Γ⇒𝐴 against Δ,𝐴,Θ⇒𝐶, the two induction hypotheses are cut free and theorem 38.6 derives Δ,Γ,Θ⇒𝐶 without cut. ◻
The residual notation can now be justified by an exact equivalence, rather than by the suggestive application trees alone.
Proof. The forward implications are exactly Slash-R and Bslash-R. For the first reverse implication, combine identities with Slash-L to obtain 𝐵/𝐴,𝐴⇒𝐵. Cut a given Γ⇒𝐵/𝐴 into its first antecedent position, obtaining Γ,𝐴⇒𝐵, and eliminate that cut by theorem 38.8. For the second, use the displayed application 𝐴,𝐴\𝐵⇒𝐵, cut a given Γ⇒𝐴\𝐵 into its second position, and eliminate the cut. The resulting word is 𝐴,Γ, not Γ,𝐴. ◻
★★☆ Let 𝑝,𝑞 be atoms and let Γ be any ordered context. Prove the derivability equivalence Γ,𝑝⇒𝑞⟺Γ⇒𝑞/𝑝. In the reverse direction, display the Slash-L derivation used as the right premise of cut, state the cut occurrence, and preserve the order Γ,𝑝 in the conclusion. Do not use an exchange rule.
★★☆ Starting only from D:Γ,𝐴,𝐵⇒𝐶, construct derivations of Γ⇒(𝐶/𝐵)/𝐴andΓ⇒𝐶/(𝐴⋅𝐵). For the second derivation, first combine 𝐴,𝐵 into a product on the left. State why the superficially similar Γ⇒(𝐴⋅𝐵)\𝐶 does not follow unless 𝐴,𝐵 occur before Γ in the premise.
Cut elimination reduces derivability to a finite backward calculation. The finiteness proof must account for both the choice of a context split and the choice of a principal antecedent formula.
The procedure 𝗌𝖾𝖺𝗋𝖼𝗁(Γ⇒𝐴) enumerates every backward instance of the seven rules:
close by Id when the context is the one-letter word 𝐴;
when 𝐴=𝑋⋅𝑌, try every split Γ=Γ0,Γ1 for Prod-R;
when 𝐴=𝑋\𝑌 or 𝑌/𝑋, try the corresponding right rule;
scan antecedent occurrences from left to right. At an occurrence 𝑋⋅𝑌, try Prod-L. At 𝑋\𝑌, write its prefix as Δ,Γ0 and enumerate those prefix splits by increasing |Δ|, trying Γ0⇒𝑋 and Δ,𝑌,Θ⇒𝐴. At 𝑌/𝑋, write its suffix as Γ0,Θ and enumerate those suffix splits by increasing |Γ0|, trying Γ0⇒𝑋 and Δ,𝑌,Θ⇒𝐴.
A branch succeeds when all of its premises succeed, and a node succeeds when at least one branch succeeds. Order branches by the numbered clauses and use the occurrence and split orders specified in clause 4. Traverse the resulting finite tree depth first. This total order fixes one reproducible trace without changing the success judgment.
For example, search on 𝑝,𝑝\𝑞⇒𝑞 rejects identity and the succedent rules, then selects the second antecedent occurrence for Bslash-L. The first prefix split 𝜖∣𝑝 makes the argument block 𝑝, producing the two identity leaves 𝑝⇒𝑝,𝑞⇒𝑞. Thus the first successful branch applies Bslash-L with Γ=𝑝, 𝐴=𝑝, 𝐵=𝑞, and empty surrounding contexts; its two premises are exactly the displayed identity leaves and its conclusion is 𝑝,𝑝\𝑞⇒𝑞.
The residual-left clauses explain why merely selecting a principal formula is not enough: the argument may consume any contiguous block on its required side, and every such block must be tried.
Proof. A right rule removes the outer connective of the succedent. Prod-L removes the product connective from one antecedent. In Prod-R, either premise omits the other result subformula, the connective joining them, and the context block assigned to the other premise. In a residual-left rule, the argument premise omits the continuation, the other residual subformula, and the residual connective; the continuation premise omits the argument block, the argument formula, and that connective. Since every formula has positive size, each omission decreases the weight. Identity has no premise. ◻
For every sequent of Lord, backward search terminates. It succeeds exactly when the sequent is derivable, and every successful branch reconstructs a cut-free derivation.
Proof of Theorem 38.13 — Decidability and exactness of search
Proof. There are finitely many antecedent occurrences and finitely many splits of a finite word, so every node has finite branching. By lemma 38.12, every branch has length at most the initial weight. The search tree is therefore finite.
For soundness, induct on a successful search tree and reapply the rule named at each node. For completeness, take any derivation. Eliminate its cuts by theorem 38.8, then induct on the resulting cut-free derivation. Its last rule is one of the seven rules, and the procedure enumerates its principal occurrence and its exact context split. The induction hypotheses give successful searches for every premise of that branch. ◻
The illegal-exchange result now applies even to derivations initially written with cut: cut elimination would produce the cut-free derivation that proposition 38.4 rules out.
A sentence is an ordered derivation
Let 𝗇𝗉 be the type of a noun phrase and 𝗌 the type of a sentence. Assign Ada⏟𝗇𝗉,likes⏟(𝗇𝗉\𝗌)/𝗇𝗉,Bert⏟𝗇𝗉. The verb first consumes its object on the right. The resulting phrase waits for its subject on the left. The complete parse is 𝑋𝗇𝗉⇒𝗇𝗉Id𝑋𝗇𝗉⇒𝗇𝗉Id𝑋𝗌⇒𝗌Id𝗇𝗉,𝗇𝗉\𝗌⇒𝗌Bslash−L𝗇𝗉,(𝗇𝗉\𝗌)/𝗇𝗉,𝗇𝗉⇒𝗌Slash−L. Read the inner inference first: a subject followed by a predicate makes a sentence. The outer inference inserts the transitive verb before the object block, exactly as Slash-L requires. Reversing the two names in the input does not change grammaticality because their categories coincide; moving the verb past either name does change the category word, and search rejects it.
Proof of Proposition 38.14 — A visible word-order failure
Proof. By cut elimination, consider a cut-free derivation. The atomic succedent precludes a right rule. The only compound antecedent is the slash formula, so the last rule must be Slash-L. That rule requires its argument context to occur to the right of the slash formula. Here the right suffix is empty, and no empty context derives the atom 𝗇𝗉, by lemma 38.3. No last rule remains. ◻
Ordered, noncommutative, planar, braided, and symmetric
These words describe different data. Treating them as synonyms hides where a crossing entered the proof.
Let Lex be Lord plus the single structural rule Δ,𝐴,𝐵,Θ⇒𝐶Δ,𝐵,𝐴,Θ⇒𝐶Ex. Thus Lord is ordered: antecedents are words and it has no rule or context equation that swaps adjacent formulas. Call a calculus noncommutative at product when some formulas 𝐴,𝐵 make 𝐴⋅𝐵⇒𝐵⋅𝐴 underivable. This is a derivability property, not another kind of context. By contrast, Lex admits every adjacent swap.
Proof of Proposition 38.16 — The exact structural boundary
Proof. By cut elimination, inspect a cut-free last rule. If it is Prod-R, a split of the one-formula antecedent leaves an empty context in the premise with atomic succedent 𝐴 or 𝐵, which is impossible by lemma 38.3. The only remaining applicable last rule is Prod-L; its premise is 𝐴,𝐵⇒𝐵⋅𝐴. Its last rule must be Prod-R, and all three splits fail by the same atomic lemma, as in proposition 38.4. In the exchange extension, derive 𝐵,𝐴⇒𝐵⋅𝐴 by two identities and Prod-R, apply Ex to obtain 𝐴,𝐵⇒𝐵⋅𝐴, and finish with Prod-L. ◻
Proof of Proposition 38.17 — Exchange identifies the two residuals
Proof. For the first sequent, derive the application 𝐴,𝐴\𝐵⇒𝐵 by Bslash-L, exchange its two antecedents, and apply Slash-R. For the second, derive 𝐵/𝐴,𝐴⇒𝐵 by Slash-L, exchange, and apply Bslash-R. Thus the ordered distinction is precisely what exchange removes; no formula equality is postulated. ◻
There are three further comparisons, but they are not extra rules of the calculus just defined. A planar drawing represents a derivation with its input leaves in antecedent order and no wire crossings. The seven rules admit such drawings because each rule joins or expands adjacent blocks. A braided presentation instead records explicit crossing generators 𝜎𝑖, identifies the two three-wire composites 𝜎𝑖𝜎𝑖+1𝜎𝑖 and 𝜎𝑖+1𝜎𝑖𝜎𝑖+1, and retains the history of a double crossing. A symmetric presentation further identifies 𝜎2𝑖 with the identity. These are equations between proof representations. The rule Ex records only derivability after a swap, so it cannot by itself distinguish braided from symmetric proof identity. We make no normalization or coherence claim for either presentation. The hexagon equations for a braiding and the additional involutivity equation for a symmetry are displayed in Baez and Stay, §§2.4–2.5, printed pp. 20–23 [BS09].
The same three-wire interface makes the distinction visible: Diagram The braided panel records a crossing generator; the symmetric panel adds the equation 𝜎2𝑖=𝗂𝖽. A planar proof has no crossing to label.
Source note.
Veltri’s normalization-by-evaluation theorem covers ordered possibly empty contexts, product, both residuals, and multiplicative unit in natural deduction [Vel22]. The cut elimination proof in theorem 38.8 and the bounded search proof in theorem 38.13 concern the sequent calculus defined in this chapter and do not depend on that imported theorem.
★★☆ Run the deterministic enumeration fixed in definition 38.11 on 𝑝,𝑝\𝑞,𝑞\𝑟⇒𝑟. List, in order, every candidate visited before and along the first successful branch, recording each selected residual and split. Display the resulting cut-free derivation and the weights on its longest branch.
★★☆ Normalize a principal Bslash-R/Bslash-L cut. Name the two smaller cut formulas and check that its final context is Δ,Σ,Γ,Θ, not a permutation of those four blocks.
★★☆ Give categories to the four-word string “Ada sends Bert mail” using atoms 𝖺,𝖻,𝗆,𝗌, assigning the three names the distinct categories 𝖺,𝖻,𝗆. Make “sends” consume 𝖻, then 𝗆, on the right and 𝖺 on the left. Derive the sentence; for each single adjacent swap, give the failed argument premise.
★★☆ For distinct atoms 𝐴,𝐵,𝐶, refute 𝐴⋅(𝐵⋅𝐶)⇒(𝐴⋅𝐶)⋅𝐵 in the ordered calculus by comparing the atomic frontiers of a cut-free derivation. Derive it in the exchange extension, mark the single crossing of 𝐵 and 𝐶, and explain why proposition 38.16 alone does not supply this derivation.
★☆☆ Let 𝜎1 cross the first two of three adjacent wires and 𝜎2 cross the last two. Read a composite 𝑓𝑔 from left to right: perform 𝑓, then 𝑔. Starting from the top order (1,2,3), list the intermediate order after every generator and verify that 𝜎1𝜎2𝜎1 and 𝜎2𝜎1𝜎2 have the same endpoint order. State what the braid equation identifies and why it does not imply 𝜎2𝑖=𝗂𝖽.
★★★Practical project.ordered-lambek-search Implement the deterministic cut-free search of definition 38.11 in Kappa. The oracle must accept product reassociation, a residuation pair, the ordered residual chain, and the distinct-category sentence, while rejecting atomic exchange and all three single adjacent sentence swaps. Mutate Prod-R so it reverses its two premise blocks; the mutant must type-check and audit cleanly but fail the association or exchange oracle. For a residual rule, the selected argument must be one contiguous antecedent block, and no step may permute the remaining word. The executable result is the six Boolean oracle lines and their all-pass summary. Administrative fuel may witness totality of the Kappa encoding; explain why that bounded run is not the mathematical descent proof of lemma 38.12. Appendix E records the four acceptance commands and appendix F gives the search stages.
Diagram The braided panel records a crossing generator; the symmetric panel adds the equation