Non-commutative Logic

Origin. Lambek calculus (1958) for linguistics. Non-commutative linear logic (Abrusci 1991). Order of hypotheses matters. Models syntactic structure. Foundation for categorial grammar.

Models. Sequents as ordered lists, not sets. A, B ≠ B, A in context. Left and right implications distinct. Planar proof nets. Pregroups and residuated structures.

Formalism.

Directional implications: A \ B: B given A on left B / A: B given A on right A • B: A followed by B (non-commutative tensor)

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

Lambek calculus rules: Right rules: A, Γ ⊢ B Γ, A ⊢ B ────────── ────────── Γ ⊢ A \ B Γ ⊢ B / A

The discharged A goes on the side the slash points to: left for , right for /.

Left rules: Δ ⊢ A Γ, B, Γ' ⊢ C ────────────────────── \L Γ, Δ, A \ B, Γ' ⊢ C

Δ ⊢ A Γ, B, Γ' ⊢ C ────────────────────── /L Γ, B / A, Δ, Γ' ⊢ C

Product (concatenation): Γ ⊢ A Δ ⊢ B ──────────────── Γ, Δ ⊢ A • B

Linguistic example: John : NP sleeps : NP \ S John sleeps : S (by \ elimination)

Cyclic variants: Cyclic linear logic: circular sequents. Mix rule restores some symmetry.

Symbols.

Symbol	Unicode	Name	Meaning
\	U+005C	Reverse solidus / Under	Left residual: A \ B seeks its A on the left
/	U+002F	Solidus / Over	Right residual: B / A seeks its A on the right
•	U+2022	Bullet / Product	Non-commutative tensor, read as concatenation
⊢	U+22A2	Turnstile	Entailment from an ordered list of hypotheses
Γ	U+0393	Gamma	A context, here a list
Δ	U+0394	Delta	Second context in the left rules
⊗	U+2297	Circled times / Tensor	The product written • in Lambek notation
⅋	U+214B	Par	Multiplicative disjunction in the cyclic linear systems
S	—	Sentence	Atomic category
NP	—	Noun phrase	Atomic category
mix	—	Mix rule	Optional rule partially restoring symmetry in cyclic systems

Metatheory. Cut elimination holds for the Lambek calculus and for Abrusci's non-commutative linear logic, and the subformula property that follows gives decidability by terminating proof search. The Lambek calculus is decidable with the product included — NP-complete (Pentus 2006), not undecidable. Recognition for a fixed Lambek grammar is polynomial, since Lambek grammars generate exactly the context-free languages (Pentus 1993). The categorical semantics is monoidal but not symmetric: dropping exchange is exactly dropping the symmetry isomorphism, and the two implications are the two adjoints that a non-symmetric tensor has instead of one. Yetter's cyclic linear logic weakens non-commutativity to invariance under cyclic permutation of the sequent, which is enough to keep a single involutive negation, and its multiplicative proof nets are the planar ones — the Danos–Regnier criterion supplemented by a planarity condition. Adding the mix rule collapses ⊗ into ⅋ in one direction and changes the correctness criterion from connected-and-acyclic to acyclic alone.

Applies to. Categorial grammar and parsing as deduction. Planar proof nets. Cyclic linear logic and non-symmetric monoidal categories. Ordered resource disciplines: stacks, queues, memory layout. Concurrency with position-sensitive resources.

Limitations. Exchange is unavailable, so a hypothesis cannot be moved and every rule is sensitive to position; this is what forces two implications where commutative systems have one, and it means the deduction theorem splits into a left and a right version neither of which subsumes the other. Generative capacity is capped at context-free for the associative Lambek calculus, so cross-serial dependencies are underivable and word orders requiring genuine permutation cannot be generated without modalities or a displacement extension. Cyclic systems recover only rotation, not permutation, so they sit strictly between the ordered and the commutative case and validate neither's full set of principles. Negation behaves badly in the fully non-commutative setting: two negations, left and right, are needed unless cyclicity is imposed, and they are not interchangeable. No non-commutative system in this family has a proof-net presentation for the additives comparable to the planar multiplicative one.