nLab irreflexive relation

In higher category theory

A (binary) relation $\sim$ on a set $A$ is irreflexive if no element of $A$ is related to itself:

$\forall \left(x:A\right),\phantom{\rule{thickmathspace}{0ex}}x\nsim x.$\forall (x: A),\; x \nsim x .

In the language of the $2$-poset Rel of sets and relations, a relation $R:A\to A$ is irreflexive if it is disjoint? from the identity relation on $A$:

${id}_{A}\cap R\subseteq \varnothing .$\id_A \cap R \subseteq \empty .

Of course, this containment is in fact an equality.

In constructive mathematics, if $A$ is equipped with a tight apartness $#$, we say that $\sim$ is strongly irrelexive if only distinct elements of $A$ are related:

$\forall \left(x:A\right),\phantom{\rule{thickmathspace}{0ex}}\forall \left(y:A\right),\phantom{\rule{thickmathspace}{0ex}}x\sim y\phantom{\rule{thickmathspace}{0ex}}⇒x#y.$\forall (x: A),\; \forall (y: A),\; x \sim y \;\Rightarrow x \# y .

Since $#$ is irrelexive itself, any strongly irrelexive relation must be irrelexive. The converse holds using excluded middle, through which every set has a unique tight apartness.

Revised on August 24, 2012 20:04:01 by Urs Schreiber (89.204.138.8)