Lab for Automated Reasoning and Analysis LARA

Partial Orders

Partial ordering relation is a binary relation $\leq$ that is reflexive, antisymmetric, and transitive, that is, the following properties hold for all $x,y,z$:

  • $x \leq x$
  • $x \leq y \land y \leq x \rightarrow x=y$
  • $x \leq y \land y \leq z \rightarrow x \leq z$

If $A$ is a set and $\le$ a binary relation on $A$, we call the pair $(A,\le)$ a partial order.

Given a partial ordering relation $\le$, the corresponding strict ordering relation $x < y$ is defined by $x \le y \land x \neq y$ and can be viewed as a shorthand for this conjunction.

We can view partial order $(A,r)$ as a first-order interpretation $I=(A,\alpha)$ of language ${\cal L}=\{\le\}$ where $\alpha({\le})=r$.

Example Partial Orders

Orders on integers, rationals, reals are all special cases of partial orders called linear orders.

Given a set $U$, let $A$ be any set of subsets of $U$, that is $A \subseteq 2^U$. Then $(A,\subseteq)$ is a partial order.

Example: Let $U = \{ 1,2,3\}$ and let $A = \{ \emptyset, \{1\}, \{2\}, \{3\}, \{2,3\} \}$. Then $(A, \le)$ is a partial order. We can draw it as a Hasse diagram.

Hasse diagram

Hasse diagram presents the relation as a directed graph in a plane, such that

  • the direction of edge is given by which nodes is drawn above
  • transitive and reflexive edges are not represented (they can be derived)

Extreme Elements in Partial Orders

Given a partial order $(A,\le)$ and a set $S \subseteq A$, we call an element $a \in A$

  • upper bound of $S$ if for all $a' \in S$ we have $a' \le a$
  • lower bound of $S$ if for all $a' \in S$ we have $a \le a'$
  • minimal element of $S$ if $a \in S$ and there is no element $a' \in S$ such that $a' < a$
  • maximal element of $S$ if $a \in S$ and there is no element $a' \in S$ such that $a < a'$
  • greatest element of $S$ if $a \in S$ and for all $a' \in S$ we have $a' \le a$
  • least element of $S$ if $a \in S$ and for all $a' \in S$ we have $a \le a'$
  • least upper bound (lub, supremum, join, $\sqcup$) of $S$ if $a$ is the least element in the set of all upper bounds of $S$
  • greatest lower bound (glb, infimum, meet, $\sqcap$) of $S$ if $a$ is the greatest element in the set of all lower bounds of $S$

Taking $S=A$ we obtain minimal, maximal, greatest, least elements for the entire partial order.

Duality minimal/maximal, least/greatest, supremum/infimum


  • minimal element need not exist: $(0,1)$ interval of rationals
  • there may be multiple minimal elements: $\{\{a\},\{b\},\{a,b\}\}$
  • if minimal element exists, it need not be least: above example
  • there are no two distinct least elements for the same set
  • least element is always glb and minimal
  • if glb belongs to the set, then it is always least and minimal
  • for relation $\subseteq$ on sets, $glb$ is intersection, $lub$ is union (not all families of sets are closed under $\cap$, $\cup$)

Monotonic functions

Given two partial orders $(C,\le)$ and $(A,\sqsubseteq)$, we call a function $\alpha : C \to A$ monotonic iff for all $x, y \in C$,

  x \leq y\ \rightarrow\ \alpha (x) \sqsubseteq \alpha (y)

partial_order.txt · Last modified: 2009/03/26 17:12 by vkuncak