Lab for Automated Reasoning and Analysis LARA


A (reflexive) preorder relation $\rho$ on set $A$ is a binary relation $r \subseteq A^2$ that is reflexive and transitive, that is, these two properties hold:

  • $x \mathop{\rho} x$
  • $x \mathop{\rho} y\ \land\ y \mathop{\rho} z \ \rightarrow\ x \mathop{\rho} z$

Constructing a partial order from a preorder

Intuitively, preorder differs from partial order in that there are distinct elements that have same ordering properties with respect to other elements. For such elements we therefore have $x \rho y$ and $y \rho x$. By identifying these elements we obtain a partial order.

More precisely, let $\rho$ be a preorder. Define relation $\sim$ by

  x \sim y \ \iff\ x \mathop{\rho} y\ \land\ y \mathop{\rho} x

It is easy to verify that $\rho$ is an equivalence relation. Moreover, if we define relation $\leq$ on equivalence classes by

  P \leq Q\ \iff\  (\forall x \in P. \forall y \in Q. x \mathop{\rho} y)

for $P, Q \in A/_{\sim}$, then we can prove that $\leq$ is a partial order.

preorder.txt · Last modified: 2007/03/30 20:52 by vkuncak