# nLab reflexive symmetric relation

## In higher category theory

#### Constructivism, Realizability, Computability

intuitionistic mathematics

foundations

# Contents

## Definition

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

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

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