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.

Symbol	Unicode	Name	Meaning
⊗	U+2297	Ordered tensor	Concatenation
\	—	Under	Left residual
/	—	Over	Right residual
⊢	U+22A2	Entails	Derivability
I	—	Unit	Empty string
Γ	U+0393	Context	Ordered list

Metatheory. 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. Cut elimination holds. Completeness for residuated semigroups (non-commutative). 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.