irreflexive comparison

Irreflexive comparison

Irreflexive comparison


Just as preorders generalise equivalence relations and total orders, irreflexive comparisons should generalise apartness relations and linear orders


An irreflexive comparison on a set SS is a (binary) relation <\lt on SS that is both irreflexive and a comparison. That is:

  • x<xx \lt x is always false;
  • If x<zx \lt z, then x<yx \lt y or y<zy \lt z

An irreflexive comparison that is also a connected relation (if x<yx \lt y is false and y<xy \lt x is false, then x=yx = y) is a connected irreflexive comparison.

If the set is an inequality space, then an irreflexive comparison is strongly connected if xyx \neq y implies x<yx \lt y or y<xy \lt x.

If an irreflexive comparison satisfies symmetry (if x<yx \lt y then y<xy \lt x then it is an apartness relation.

If a connected irreflexive relation is also symmetric (if x<yx \lt y, then y<xy \lt x), then it is a tight apartness relation, and if it is transitive (if x<yx \lt y and y<zy \lt z, then x<zx \lt z), then it is a linear order.

Thus, irreflexive comparisons are dual to preorders while connected irreflexive comparisons are dual to partial orders.


A set SS equipped with an irreflexive comparison is a category (with SS as the set of objects) enriched over the cartesian monoidal category TV opTV^\op, that is the opposite of the poset of truth values, made into a monoidal category using disjunction. TV opTV^\op is a co-Heyting algebra.

Created on May 27, 2021 at 09:43:29. See the history of this page for a list of all contributions to it.