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: right residual ("A under B" — given A on left, produces B)
• B / A: left residual ("B over A" — given A on 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 \ B) ⊗ A ⊢ B (apply function on right) A ⊗ (A \ B) ⊬ B (wrong order!)

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. Lambek calculus decidable (polynomial). Cut elimination holds. Completeness for residuated semigroups (non-commutative). NP-complete for some extensions. Proof nets: geometric representation. Embedding: exchange makes it linear logic; weakening+contraction makes it intuitionistic.

Applies to. Computational linguistics (categorial grammar). Stack-based computation. Process ordering. Non-commutative quantum mechanics. Formal language theory. Type-logical grammar.

Limitations. More restrictive than linear logic. Limited applications outside linguistics. Exchange often needed for practical reasoning. Proof search harder without symmetry. Tool support specialized. Extensions (modalities) increase complexity. Natural language often allows reordering.

© 2026 Lingenic LLC