A (binary) relation on a set is irreflexive if no element of is related to itself:
In the language of the -poset Rel of sets and relations, a relation is irreflexive if it is disjoint? from the identity relation on :
Of course, this containment is in fact an equality.
In constructive mathematics, if is equipped with a tight apartness , we say that is strongly irrelexive if only distinct elements of are related:
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