nLab reflexive symmetric relation



Constructivism, Realizability, Computability

Equality and Equivalence



The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



An reflexive symmetric relation is a binary relation that is reflexive and symmetric.


In constructive mathematics

In constructive mathematics, the double negation of equality cannot in general be proven to be an equivalence relation, because the denial inequality cannot be proved to be an apartness relation. Instead, the double negation of equality is only a stable reflexive symmetric relation. Indeed, since excluded middle cannot be proven, we could distinguish between the following reflexive symmetric relations in constructive mathematics:

  • equality

  • equivalence relations, a transitive reflexive symmetric relation

  • double negation of equality

  • stable reflexive symmetric relation, a reflexive symmetric relation \approx which additionally satisfies ¬¬(ab)\neg \neg (a \approx b) implies aba \approx b

  • decidable reflexive symmetric relation, an reflexive symmetric relation \approx which additionally satisfies (ab)(a \approx b) or ¬(ab)\neg (a \approx b)

 See also

Created on December 8, 2022 at 20:33:44. See the history of this page for a list of all contributions to it.