Called respectively right and left residuals, these operations coincide when the monoid is commutative.
More precisely, for a given x in L, the unary operations x• and x\ are respectively the lower and upper adjoints of a Galois connection on L, and dually for the two functions •y and /y.
By the same reasoning that applies to any Galois connection, we have yet another definition of the residuals, namely, together with the requirement that x•y be monotone in x and y.
This last definition is purely in terms of inequalities, noting that monotonicity can be axiomatized as x • y ≤ (x∨z) • y and similarly for the other operations and their arguments.
However distributivity of ∧ over ∨ is entailed when • and ∧ are the same operation, a special case of residuated lattices called a Heyting algebra.
Given two ideals A and B in Id(R), the residuals are given by It is worth noting that {0}/B and B\{0} are respectively the left and right annihilators of B.
The structure (Z, min, max, +, 0, −, −) (the integers with subtraction for both residuals) is a commutative residuated lattice such that the unit of the monoid is not the greatest element (indeed there is no least or greatest integer), and the multiplication of the monoid is not the meet operation of the lattice.
Any totally ordered group under addition such as the rationals or the reals can be substituted for the integers in this example.
The left residual is the mirror image of this: y(S/R)x holds just when for all z in X, xRz implies ySz.
In natural language residuated lattices formalize the logic of "and" when used with its noncommutative meaning of "and then."
"[citation needed] Humans do not so readily detect that Peirce's law ((P→Q)→P)→P is a classical tautology, an interesting situation where humans exhibit more proficiency with non-classical reasoning than classical (for example, in relevance logic, Peirce's law is not a tautology).[relevant?]
Thus it is an algebraic structure L = (L, ∨, •, 1, /, \) satisfying all the residuated lattice equations as specified above except those containing an occurrence of the symbol ∧.