Depending on the chosen perspective on foundations this is either an axiom or a consequence of the axiom of choice; or neither if neither the axiom of choice nor Zorn’s lemma is assumed as an axiom. Conversely, Zorn's lemma and the axiom of excluded middle together imply the axiom of choice. Although it doesn't imply excluded middle itself, Zorn's lemma is not generally accepted in constructive mathematics as an axiom.
(Say something about how one can systematically get around this in many situations ….)
In as far as it holds or is assumed to hold, Zorn’s lemma is a standard method for constructing (or at least, proving the existence of) objects that are ‘maximal’ in an appropriate sense. It is commonly used in algebra and named after the algebraist Max Zorn (although he himself protested the naming after him).
The proposition Zorn's Lemma states that each preordered set has a maximal element if every chain in has an upper bound.
Suppose the axiom of choice holds. Then Zorn's Lemma holds.
By contradiction. (A direct proof of the existence of a maximal element is not possible, so we freely use the axiom of excluded middle, which in any case follows from AC, the axiom of choice. The one use made of AC is noted below. WLOG we prove the result for posets.)
Suppose has no maximal element. Then every chain has a strict upper bound: an element such that for all . (Take an upper bound of , then is not maximal by supposition, so any with will serve.) For each that is well-ordered by , use AC to choose a strict upper bound of . Given a such a function from well-ordered subsets of to , let us say is -inductive if for every , we have .
Let be -inductive sets; we will show one is an initial segment of the other. Let be the union of all subsets that are initial segments of both and ; then is maximal among initial segments of both (possibly empty). Suppose is properly contained in both; let be the least element of , and the least element of . Then , so by -inductivity of , we have . Thus extends to an initial segment , contradicting maximality of . Therefore we must have or , so one of is an initial segment of the other.
So the collection of -inductive sets is totally ordered by inclusion of initial segments, making their union the maximal -inductive set (Lemma 1 below). Appending its strict upper bound , the chain is a larger -inductive set, contradiction. The proof is complete.
The empty set is not an exception to Zorn's lemma, as the chain does not have an upper bound.
The proof above (does anyone know where it appears in the literature?) can be seen as an application of general recursion theory à la Paul Taylor’s book, which in turn is inspired in large part by Osius. In particular, initial segments are the same as -coalgebra maps between well-founded coalgebras, and the maximal constructed is a maximal attempt with respect to a partial algebra structure , following Taylor’s formulation of the recursion scheme. For a slightly different arrangement of the facts, one very commonly found in the literature, see the account of the Bourbaki-Witt theorem below.
Let be a collection of subsets of a set , each equipped with a well-ordering , such that for any , one of (each with their orderings) is an initial segment of the other. Let be the union , equipped with the ordering if in some containing them both. Then is well-ordered by , with each an initial segment of .
Observe that is well-defined, and is a total order: if , then and for some , where one of contains the other, say , whence are comparable in . If is an inhabited subset of , then is inhabited for some , so there is a minimal element with respect to . This is minimal in with respect to , for if , , then by the initial segment condition, and then by definition of .
Let be a set, and consider the poset whose elements are pairs , where and is a (classical) well-ordering on , ordered by if as a well-ordered set is an initial segment of . If is a chain in the poset consisting of subsets , then their union is a well-order by Lemma 1, and so the hypothesis of Zorn’s lemma is satisfied.
By Zorn’s lemma, conclude that the poset above contains a maximal element , where . We claim ; suppose not (here is where we need excluded middle), and let be a member of the complement . Well-order , extending by deeming to be the final element. This shows was not maximal, contradiction. Hence any set may be well-ordered.
The axiom of choice follows: suppose given a surjection , so that every fiber is inhabited. Consider any well-ordering of , and define by letting be the least element in with respect to the well-ordering. This gives a section of .
Many accounts of the proof of Zorn’s lemma start by establishing first the so-called Bourbaki-Witt theorem, which does not require AC and is of interest in its own right. However, it too does not admit a constructive proof; see Bauer for a demonstration that it is not valid in the effective topos. That said, the issue is subtle enough that the Bourbaki-Witt theorem nonetheless holds in topos with a geometric morphism to , for instance any Grothendieck topos, assuming B-W holds in (Bauer-Lumsdaine 2013).
Without loss of generality, assume has a bottom element ; otherwise just pick an element and replace with the upward set .
Say that a subset is -inductive if: , is closed under (), and contains the sup of any chain in . The intersection of any family of -inductive sets is also -inductive, so the intersection of all -inductive sets is -inductive.
The idea is that is totally ordered (is a chain) by the following intuition: the elements of are , where we continue by transfinite induction: at limit ordinals define to be the sup of , and at successors define . We cannot have a strictly increasing chain that goes on forever, by cardinality considerations, so at some point we hit an such that , which provides a fixed point. (What could be nonconstructive about that? See this comment by Lumsdaine.) In any case, once we prove is totally ordered, the sup of is obviously a fixed point.
Without getting into ordinals, one may prove is totally ordered as follows. Call an element a cap if for implies . For each , put . A routine verification shows is -inductive if is a cap, so in fact by minimality of . Then, show that the set of caps is -inductive. This is also routine if we avail ourselves of the just-proven fact that for any cap (but consult Appendix 2 in Lang’s Algebra if you get stuck). So again by minimality of , every element of is a cap. Finally, if , use the fact that is a cap to conclude either that or , whence ; thus we see any two elements are comparable.
For a discussion of how to get from Bourbaki-Witt to Zorn, see either Lang or this -Category Café post by Tom Leinster, especially the main post which gives three very closely related results bearing on Zorn’s lemma, and a follow-up comment here which brings in Bourbaki-Witt.
An alternative proof of Bourbaki-Witt would be along lines similar to those used to show AC implies Zorn’s lemma. Given the inflationary function , consider the function which takes a well-ordered subset to . If has no fixed points, then will always be a strict upper bound of , and from there one derives a contradiction exactly as in the proof of Zorn’s lemma.
The Bourbaki-Witt theorem is an example of a fixed-point theorem. We should point out its kinship with the quite remarkable fixed-point theorem due to Pataraia, who observed that the conclusion of the Bourbaki-Witt theorem may be strengthened quite considerably, and proved constructively (!), if we change the hypothesis to say that is a monotone operator (preserves the order ) on an inhabited dcpo. See fixed point for a brief account, and this blog post for some appreciative commentary.
It is very common, when starting with a preordered set , to apply Zorn's lemma not to itself but to an up-set (an under category) in . That is, one starts with an element of and proves the existence of a maximal element comparable to .
Zorn's lemma may be used to prove all of the following:
Some of these are equivalent to Zorn's lemma, while some are weaker; conversely, some additionally require excluded middle.
Serge Lang, Algebra (third edition), Addison-Wesley 1993.
Gerhard Osius, Categorical set theory: a characterization of the category of sets, Jour. Pure Appl. Alg. 4 (1974), 79-119. doi:10.1016/0022-4049(74)90032-2
Andrej Bauer, On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos, Electronic Notes in Theoretical Computer Science, 249 (2009) pp 157-167, doi:10.1016/j.entcs.2009.07.089 and Theoretical Computer Science, 430 (2012) pp 43-50, doi:10.1016/j.tcs.2011.12.005. arXiv:0911.0068.