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

Left rules: Δ ⊢ A Γ, B, Γ' ⊢ C ────────────────────── Γ, Δ, A \ B, Γ' ⊢ 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
\	—	Under	Left residual
/	—	Over	Right residual
•	—	Product	Non-comm tensor
⊢	U+22A2	Turnstile	Entailment

Metatheory. Cut elimination. Decidable for Lambek calculus. Undecidable with product. Categorical semantics: monoidal categories (not symmetric). NL-completeness for recognition.

Applies to. Categorial grammar. Type-logical semantics. Natural language parsing. Linguistic syntax. Word order analysis.

Limitations. Linguistically limited without modalities. Parsing complexity. Doesn't handle all word orders. Less tool support than commutative variants.