nLab denial inequality



Equality and Equivalence



The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



A weak inequality relation or denial inequality relation \neq on a set SS is the negation of the equality relation on SS.

ab¬(a=b)a \neq b \coloneqq \neg(a = b)

This is a term found in constructive mathematics, to distinguish from strict inequality relation or other notions of inequality relation such as tight apartness relations. In classical mathematics, weak inequality relations and strict inequality relations are the same and are simply called “inequality”, so the notion plays no further role classically.

If one wishes to reserve the word “inequality” for order relations (such as \le and <\lt), then one may instead use the word disequality to refer to the weak inequality. (For instance, this is common in type theory with subtype relations that form an ordering on the types.)


The weak inequality relation is an irreflexive symmetric relation. Irreflexivity follows from the negation of reflexivity of equality, while symmetry follows from the contrapositive of symmetry of equality. In addition, the weak inequality relation is a stable relation, because in constructive mathematics, given any proposition PP, ¬¬¬P\neg \neg \neg P implies that ¬P\neg P. This means that ¬¬¬(a=b)\neg \neg \neg (a = b) implies that ¬(a=b)\neg (a = b), and since ¬(a=b)\neg (a = b) if and only if aba \neq b, this means that ¬¬(ab)\neg \neg (a \neq b) implies that aba \neq b. Weak inequality is a weakly tight relation, in that for all elements aAa \in A and bAb \in A, ¬(ab)\neg (a \neq b) implies that ¬¬(a=b)\neg \neg (a = b), because by definition, ¬(a=b)\neg (a = b) if and only if aba \neq b, and so by contraposition, ¬¬(a=b)\neg \neg (a = b) if and only if ¬(ab)\neg (a \neq b).

Denial apartness

The denial inequality relation on a set SS is said to be a denial apartness relation if for all elements aSa \in S, bSb \in S and cSc \in S, ¬((ab)(bc))\neg((a \neq b) \wedge (b \neq c)) implies that ¬(ab)¬(bc)\neg(a \neq b) \vee \neg(b \neq c).

This implies that \neq is an apartness relation because the contrapositive of the transitive property of equality states that aca \neq c implies that ¬((a=b)(b=c))\neg((a = b) \wedge (b = c)), and the above condition implies that ¬(ab)¬(bc)\neg(a \neq b) \vee \neg(b \neq c), which is precisely the condition for a comparison.

In particular, if de Morgan's law holds in the logic, then every weak inequality relation is a denial apartness relation.

Similarly, every stable tight apartness relation is a denial apartness relation.

See also

Last revised on December 9, 2022 at 14:55:21. See the history of this page for a list of all contributions to it.