nLab strict order



A strict order is a linear order which is not a linear relation. Strict orders are used in models of the real numbers which have infinitesimals, such as in the smooth real numbers in synthetic differential geometry, and thus where not every real number not greater than or less than zero is equal to zero.


A strict order is a binary relation <\lt on a set SS which is irreflexive, asymmetric, transitive, and a comparison:

  1. for all aSa \in S, ¬(a<a)\neg(a \lt a)

  2. for all aSa \in S and bSb \in S, if a<ba \lt b, then ¬(b<a)\neg(b \lt a)

  3. for all aSa \in S, bSb \in S, and cSc \in S, if a<ba \lt b and b<cb \lt c, then a<ca \lt c

  4. for all aSa \in S, bSb \in S, and cSc \in S, if a<ca \lt c, then a<ba \lt b or b<cb \lt c


The negation of a strict order is a preorder ab¬(b<a)a \leq b \coloneqq \neg(b \lt a), and thus has an equivalence relation defined as ababbaa \approx b \coloneqq a \leq b \wedge b \leq a. Every strict order which is also a linear relation is a linear order, whose negation is a partial order. Thus, in any foundations with quotient sets, every strict order can be made into a linear order by taking the quotient with respect to the equivalence relation S/S/\approx.

 See also


Strict orders are used in defining the smooth real numbers in:

Last revised on December 7, 2022 at 15:05:14. See the history of this page for a list of all contributions to it.