Residuated Lattices

Origin. Ward, Dilworth (1939). Algebraic semantics. Substructural foundation. Residuation. Unifying algebraic structure.

Models. Lattices with monoid. Residuation property. Substructural algebraic semantics. Generalized implication.

Formalism.

Residuated lattice: ⟨L, ∧, ∨, ·, , /, e⟩ where: ⟨L, ∧, ∨⟩: lattice. ⟨L, ·, e⟩: monoid. , /: left/right residuals.

Residuation: a · b ≤ c iff a ≤ c / b iff b ≤ a \ c. Galois connection. Adjunction. Implication from fusion.

Right residual: c / b = max{a : a · b ≤ c}. "c divided by b." Right implication.

Left residual: a \ c = max{b : a · b ≤ c}. "a under c." Left implication.

Commutative case: If · commutative: a \ c = c / a. Single residual →. a · b ≤ c iff a ≤ b → c.

Logical interpretation: ·: fusion/tensor. , /: implications. ∧, ∨: meet, join. e: unit/truth.

Substructural correspondence: FL-algebras: full Lambek. Relevance algebras: ·, → with conditions. Heyting: a · b = a ∧ b. Boolean: classical.

Varieties: Integral: a ≤ e. Contractive: a ≤ a · a. Commutative: a · b = b · a. Different logics.

Symbols.

Symbol	Unicode	Name	Meaning
·	U+00B7	Fusion	Monoid multiplication; intensional conjunction
\	—	Left residual	a \ c = max{b : a · b ≤ c}
/	—	Right residual	c / b = max{a : a · b ≤ c}
e	—	Monoid unit	Identity of fusion; the logic's truth constant
≤	U+2264	Lattice order	a ≤ b iff a ∧ b = a
∧	U+2227	Meet	Additive conjunction
∨	U+2228	Join	Additive disjunction
→	U+2192	Implication	The single residual in the commutative case
⟨L, ∧, ∨, ·, , /, e⟩	—	Residuated lattice	The signature of the variety
FL	—	Full Lambek calculus	The logic whose algebras these are

Metatheory. Residuated lattices form a variety: the residuation condition a · b ≤ c iff b ≤ a \ c iff a ≤ c / b is equivalent to finitely many equations, so the class is closed under homomorphic images, subalgebras, and products and Birkhoff's theorem applies. Because there is a lattice reduct the variety is congruence-distributive, and it is congruence-permutable as well; congruences correspond bijectively to convex normal subalgebras, which is the algebraic form of the deduction theorem. Pointed residuated lattices — FL-algebras — are the equivalent algebraic semantics of the full Lambek calculus in the sense of Blok and Pigozzi, so completeness for a substructural logic becomes a statement about a subvariety: Heyting algebras are the integral commutative ones with idempotent fusion, MV-algebras add divisibility and involution, lattice-ordered groups are those with a \ b = a⁻¹b. Cut elimination for FL (Ono and Komori, 1985) yields decidability of the equational theory, and Blok and van Alten (2002) proved the finite embeddability property for integral residuated lattices, making their universal theories decidable.

Applies to. Substructural logic. Fuzzy logic. Relevance logic. Lambek calculus.

Limitations. The generality comes from dropping structural rules, and the corresponding inequalities go with them: without weakening a · b ≤ a fails, without contraction a ≤ a · a fails, and without exchange the two residuals are genuinely distinct, so there is no single implication connective. Restoring structural rules does not restore good behaviour — contraction in particular destroys decidability, as Urquhart's 1984 proof that the relevance logics R, E, and T are undecidable shows, and the corresponding varieties inherit it. Lattice distributivity is not part of the definition and must be assumed separately, so results split into distributive and non-distributive cases. The framework is purely algebraic and yields no relational semantics: frame completeness for a subvariety is a further theorem, not a corollary. Conventions differ across the literature, with \ and / interchanged by some authors, so every equation is convention-relative.