Partial order and partially ordered set

Let $P$ be a set. A partial order on $P$ is a binary relation $\le$ on $P$ such that, for all $x, y, z \in P$:

• (R) reflexivity: $x \le x$;
• (A) antisymmetry: if $x \le y$ and $y \le x$, then $x = y$;
• (T) transitivity: if $x \le y$ and $y \le z$, then $x \le z$.

The pair $(P, \le)$ is a partially ordered set, abbreviated poset. When the order is clear we write $P$ for the pair.

The associated strict order is defined by $x < y \quad :\Longleftrightarrow \quad x \le y \text{ and } x \ne y.$

Two elements $x, y \in P$ are comparable if $x \le y$ or $y \le x$, and incomparable otherwise. A partial order in which every two elements are comparable is a total order (equivalently a linear order), and $(P, \le)$ is then a totally ordered set.

• Partiality is the whole point: a partial order is permitted to leave pairs incomparable, which is what makes maximal elements and chains worth distinguishing at all. In a total order every subset is a chain, and a maximal element is automatically the greatest element.
• All three axioms are used essentially in the proofs that rest on this definition: reflexivity in The cut at an extremal element is closed under $f$ ↗ and The image of an extremal element is extremal ↗, transitivity almost everywhere, and antisymmetry in Bourbaki–Witt fixed point theorem ↗, where the fixed point is obtained by passing from $f(c) \le c$ and $c \le f(c)$ to $f(c) = c$. Antisymmetry is also what makes a least upper bound unique when it exists, and uniqueness is what licenses the functional notation $\sup$ used in Chain-complete poset ↗.
• Dropping antisymmetry gives a preorder. Preorders are genuinely useful elsewhere (a directed set is preordered).
• Inclusion $\subseteq$ on the power set of any set is the standard example, and it is the order that appears concretely in Zorn's lemma ↗, which applies Bourbaki–Witt fixed point theorem ↗ to the set of chains of $P$ ordered by inclusion, and in Zorn's lemma implies the Axiom of Choice ↗, which applies Zorn's lemma to partial choice functions ordered by extension, an inclusion order on their graphs. The results themselves are stated for an arbitrary poset and are used that way: Zorn's lemma ↗ is applied to whatever poset a later page brings, and the refutation in FALSE: every maximal element is a greatest element ↗ runs in a bare two-element antichain that is not presented as an order by inclusion at all.