Ordered Logic

Origin. Ordered (non-commutative) logic from Lambek calculus (1958) and later work. No exchange rule: order of hypotheses matters. Models resource order, linguistic word order. Part of substructural logic family. Categorical: non-symmetric monoidal categories.

Models. Order-sensitive reasoning. Linear logic: use each premise once. Ordered logic: additionally, order matters. A ⊗ B ≠ B ⊗ A in general. Models stacks, queues, left-to-right processing. Grammar: word order constraints.

Formalism.

Structural rules:

• Exchange: ✗ (order matters)
• Weakening: ✗ (linear)
• Contraction: ✗ (linear)

Ordered connectives:

• A ⊗ B: ordered tensor (A then B)
• A \ B: left residual ("A under B" — given an A on its left, produces B)
• B / A: right residual ("B over A" — given an A on its right, produces B)

Residuation laws: A ⊗ B ⊢ C iff B ⊢ A \ C iff A ⊢ C / B

Sequent calculus: No exchange rule: Γ is a list, not multiset. A, B, C different from B, A, C.

Examples: A ⊗ (A \ B) ⊢ B — the argument sits to the left, which is what \ demands. (A \ B) ⊗ A ⊬ B — wrong order. This is exactly the residuation law above with C := B.

Lambek calculus L: Original ordered logic for syntax. Categories: NP, S, N, etc. transitive_verb : (NP \ S) / NP "John sees Mary" : NP ⊗ ((NP \ S) / NP) ⊗ NP ⊢ S

Symbols.

Metatheory. Cut elimination holds, and with it the subformula property, so derivability is decidable by terminating proof search on a fixed sequent. The Lambek calculus is decidable but NP-complete (Pentus 2006) — the polynomial claim once in circulation is false for the calculus itself, and holds only of restricted fragments. The calculus is sound and complete for residuated semigroups, and adding the unit gives completeness for residuated monoids; the residuation triple A ⊗ B ⊢ C iff B ⊢ A \ C iff A ⊢ C / B is a definition rather than an axiom scheme, in that it determines both residuals uniquely from ⊗. Pentus (1993) proved that Lambek grammars generate exactly the context-free languages, so recognition for a fixed grammar is polynomial even though derivability is not. The structural rules are what separate the systems: adding exchange yields intuitionistic linear logic, and adding weakening and contraction on top yields intuitionistic logic, so ordered logic is the base of the substructural hierarchy rather than a variant of linear logic.

Applies to. Ordered logic programming and ordered logical frameworks. Stack and queue disciplines in type systems. Memory layout and adjacency constraints. Categorial grammar. The base of the substructural hierarchy.

Limitations. Exchange is unavailable, and with it every principle that depends on moving a hypothesis: the deduction theorem splits into a left and a right form, neither implication subsumes the other, and there is no single negation. Weakening and contraction are absent as well, so a hypothesis can be neither discarded nor reused, and there is no exponential in the base calculus to reintroduce them at controlled positions. Generative capacity is capped at context-free, so the cross-serial dependencies that motivate mildly context-sensitive grammars are underivable and require modalities, displacement or Grishin interaction. Associativity is a global choice: L cannot see constituent structure, while the non-associative NL can but then cannot hypothesize a gap at an unbracketed position. Categorical semantics is monoidal but not symmetric, so the coherence results and string-diagram calculi available for symmetric monoidal categories do not transfer unchanged.

© 2026 Lingenic LLC