Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
basic constructions:
strong axioms
further
A weak inequality relation or denial inequality relation $\neq$ on a set $S$ is the negation of the equality relation on $S$.
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 $P$, $\neg \neg \neg P$ implies that $\neg P$. This means that $\neg \neg \neg (a = b)$ implies that $\neg (a = b)$, and since $\neg (a = b)$ if and only if $a \neq b$, this means that $\neg \neg (a \neq b)$ implies that $a \neq b$. Weak inequality is a weakly tight relation, in that for all elements $a \in A$ and $b \in A$, $\neg (a \neq b)$ implies that $\neg \neg (a = b)$, because by definition, $\neg (a = b)$ if and only if $a \neq b$, and so by contraposition, $\neg \neg (a = b)$ if and only if $\neg (a \neq b)$.
The denial inequality relation on a set $S$ is said to be a denial apartness relation if for all elements $a \in S$, $b \in S$ and $c \in S$, $\neg((a \neq b) \wedge (b \neq c))$ implies that $\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 $a \neq c$ implies that $\neg((a = b) \wedge (b = c))$, and the above condition implies that $\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.
Last revised on January 18, 2024 at 15:07:27. See the history of this page for a list of all contributions to it.