Preorder

🅟 Feb 22, 2026

  🅤 Apr 04, 2026

DEF-PRO. Preorder.

  • A preorder is a binary relation that is reflexive and transitive.

  • If $\preceq$ is a preorder, then $\prec$ refers to the relation defined by

    \[x\prec y \enspace\lrimp\enspace x\preceq y\land x\neq y.\]

REM-PRO-S.

There is no “strict preorder”, i.e. a binary relation that is irreflexive and transitive, because such a relation is automatically asymmetric, making it a strict partial order. See PROP-PO-ASY.