Zorn lemma states that a nonempty partially ordered set in which every chain in a partial order has an upper bound has a maximal element. Here is a proof from the axiom of choice and Hartogs theorem.
Suppose there is no maximal element. Every chain has a strict upper bound: choose an upper bound and then an element strictly greater than . The family of sets of strict upper bounds is a set of nonempty subsets of the underlying set . The axiom of choice is used here to choose, simultaneously for every chain , one strict upper bound .
By Hartogs theorem there is an ordinal admitting no injection into . Transfinite recursion defines for by
At each stage the previous elements form a chain, and is strictly above every one of them. Hence is an injection , a contradiction. Therefore a maximal element exists.
Replace the strict partial order by its reflexive closure . Partially order all partial orders on extending by inclusion. A chain has an upper bound given by its union: transitivity and antisymmetry each concern finitely many pairs, which all lie in one member of the chain. By Zorn lemma there is a maximal extension .
If are incomparable under , define
This adds . It is transitive: composing an old pair with a new one stays in the added set; composing two new pairs would require , which is impossible. It is antisymmetric: an added pair and a reverse old pair would again imply , and two reverse added pairs would do the same. Thus is a larger partial order, contradicting maximality. Therefore is total, and removing its diagonal gives a total order extending the original strict order.
A well-founded relation has a minimal element in every nonempty subset; with the axiom of choice this is equivalent to having no infinite strictly descending sequence. If an extension is a well-order, its least element in any nonempty subset is minimal for the original relation, so the original order must be well-founded.
However not every total extension need be a well-order. Take the empty strict order on , which is well-founded. Its extension defined by if in the usual order is total and has no least element.

Articles by others on the same topic (0)

There are currently no matching articles.