irreflexive relation



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

(x:A),xx. \forall (x: A),\; x \nsim x .

(where xxx\nsim x means that xxx\sim x is false, i.e. that ¬(xx)\neg (x\sim x)).

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

id AR. \id_A \cap R \subseteq \empty .

Of course, this containment is in fact an equality.

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

(x:A),(y:A),xyx#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.


  • A digraph is a graph in which the edge relation is irreflexive.

Revised on September 1, 2017 14:46:59 by Urs Schreiber (