# nLab irreflexive symmetric relation

## In higher category theory

#### Constructivism, Realizability, Computability

intuitionistic mathematics

foundations

# Contents

## Definition

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

## In constructive mathematics

In constructive mathematics, not ever tight irreflexive symmetric relation is a denial inequality, and not every denial inequality is tight. Instead, every denial inequality is only weakly tight. Indeed, since excluded middle cannot be proven, we could distinguish between the following irreflexive symmetric relations in constructive mathematics:

• denial inequality, an irreflexive symmetric relation $\neq$ which additionally satisfies $\neg(a = b)$ implies $(a \neq b)$

• tight irreflexive symmetric relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $\neg(a \neq b)$ implies $(a = b)$

• weakly tight irreflexive symmetric relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $\neg(a \neq b)$ implies $\neg \neg (a = b)$

• stable irreflexive symmetric relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $\neg \neg (a \neq b)$ implies $(a \neq b)$

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

• apartness relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $a \neq b$ implies that $a \neq c$ or $c \neq b$

or any combination of the above, such as tight apartness relation.

The notion of “inequality relation” in constructive mathematics usually refers to either the denial inequality or a tight apartness relation. On the other hand, some authors have used “inequality relation” to refere to general irreflexive symmetric relations.