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 .

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.

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