Full Lambek Calculus (FL)

Origin. Lambek's syntactic calculus (1958) supplies the residuated core; the additives and constants were added and the family systematized by Ono and Komori (1985) and Ono (1993, 2003). Galatos, Jipsen, Kowalski, and Ono, Residuated Lattices: An Algebraic Glimpse at Substructural Logics (2007), is the standard reference and the reason FL is the base of the field rather than one system in it.

Models. The substructural logic with no structural rules at all beyond what a sequent calculus needs to function: no exchange, no weakening, no contraction. Everything else in the division — linear, affine, relevant, ordered, BCK, intuitionistic, classical — is FL plus a subset of the rules put back. That makes FL the origin of the coordinate system rather than a point in it, which is why the algebra came to be named after its models rather than after any of the logics.

Formalism.

Language: Fusion (product): · Two implications: \ (left residual), / (right residual) Additives: ∧, ∨ Constants: 1, 0, ⊤, ⊥

Residuation — the defining law: a · b ≤ c iff b ≤ a \ c iff a ≤ c / b Two implications because · is not commutative: what divides on the left is not what divides on the right.

Sequents: Γ ⊢ A, with Γ an ordered sequence. No exchange: Γ, A, B, Δ ⊢ C does not give Γ, B, A, Δ ⊢ C. No weakening: Γ ⊢ C does not give Γ, A ⊢ C. No contraction: Γ, A, A ⊢ C does not give Γ, A ⊢ C.

The extensions — each rule named: FLe + exchange (commutative; both implications collapse to one) FLw + weakening (affine) FLc + contraction FLew + exchange, weakening FLec + exchange, contraction FLewc = intuitionistic logic Adding involutive negation to FLe gives multiplicative-additive linear logic. The lattice of substructural logics is the lattice of these choices.

Algebraic semantics: FL is complete for FL-algebras: residuated lattices with an extra constant 0. The correspondence is exact — subvarieties of residuated lattices are the substructural logics, and the rules correspond to equations (exchange ↔ commutativity, weakening ↔ integrality, contraction ↔ square-increasingness).

Cut elimination: Holds for FL and for each extension by structural rules. Gives decidability for FL and FLe; FLec is decidable, FLc is not known in general.

Symbols.

Symbol	Unicode	Name	Meaning
·	U+00B7	Fusion	Non-commutative product
\	—	Left residual	a \ c: what a needs to give c
/	—	Right residual	c / b: what gives c with b
FLe, FLw, FLc	—	Extensions	By exchange, weakening, contraction
1, 0	—	Constants	Multiplicative unit; the residuation zero
≤	U+2264	Order	The lattice order of the algebra

Metatheory. The correspondence between structural rules and equations is what makes the division algebraic rather than merely proof-theoretic: adding exchange to the calculus is adding commutativity to the algebra, and the lattice of substructural logics is a lattice of subvarieties of residuated lattices. That is the result GJKO is organized around, and it is why the algebra was the entry in this collection before the calculus was. Cut elimination is uniform across the family; decidability is not, and the boundary — FLc's undecidability in the presence of contraction without weakening — is where the proof-theoretic and algebraic accounts stop agreeing about what is hard.

Applies to. The base for every logic in Structural. The algebraic study of substructural logics. Categorial grammar, where the non-commutative fragment without additives is the Lambek calculus. Fuzzy logic, since MTL and BL are FLew plus prelinearity and divisibility — the t-norm logics are substructural logics with weakening.

Limitations. FL is a base rather than a logic anyone reasons in: with no structural rules, contexts are sequences whose order and multiplicity both matter, and almost nothing familiar is derivable. The two implications are a symptom of that — natural language and mathematics both assume exchange, so the left/right distinction is machinery kept for the extensions' sake. The uniformity claim also hides work: adding a structural rule is easy proof-theoretically and the corresponding equation is not always obvious, and several natural substructural logics have no known rule presentation.