CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> Zorn's lemma in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> Zorn's lemma </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/4303/#Item_7" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Zorns Lemma</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+tight+apartness">axiom of tight apartness</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="zorns_lemma">Zorn's Lemma</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#statement_and_proofs'>Statement and proofs</a></li> <li><a href='#bourbakiwitt_theorem'>Bourbaki-Witt theorem</a></li> <li><a href='#wellordered_formulation'>Well-ordered formulation</a></li> <li><a href='#usageapplications'>Usage/applications</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p><em>Zorn's lemma</em>, also known as Kuratowski-Zorn lemma, is a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> in <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> and <a class="existingWikiWord" href="/nlab/show/order+theory">order theory</a>. It says that: <em>A <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a> in which every sub-<a class="existingWikiWord" href="/nlab/show/total+order">total order</a> has an <a class="existingWikiWord" href="/nlab/show/upper+bound">upper bound</a> has a <a class="existingWikiWord" href="/nlab/show/maximal+element">maximal element</a>.</em></p> <p>Depending on the chosen perspective on <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> this is either an <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a> or a <a class="existingWikiWord" href="/nlab/show/deduction">consequence</a> of the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>; or neither if neither the axiom of choice nor Zorn’s lemma is assumed as an axiom. Conversely, Zorn's lemma and the <a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a> together imply the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>. Although it doesn't imply excluded middle itself, Zorn's lemma is not generally accepted in <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a> as an <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a>. Sometimes the maximal element is only a convenience, and it’s enough to use the entire poset or perhaps the collection of all chains instead; sometimes, the use of Zorn’s Lemma is essential.</p> <p>In as far as it holds or is assumed to hold, Zorn’s lemma is a standard method for constructing (or at least, <a class="existingWikiWord" href="/nlab/show/proof">proving</a> the <a class="existingWikiWord" href="/nlab/show/existence">existence</a> of) objects that are ‘maximal’ in an appropriate sense. It is commonly used in <a class="existingWikiWord" href="/nlab/show/algebra">algebra</a> and named after the algebraist <a class="existingWikiWord" href="/nlab/show/Max+Zorn">Max Zorn</a> (although he himself protested the naming after him).</p> <h2 id="statement_and_proofs">Statement and proofs</h2> <div class="num_defn" id="ChainAndUpperBound"> <h6 id="definition">Definition</h6> <ul> <li> <p>Given a <a class="existingWikiWord" href="/nlab/show/preorder">preordered</a> set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>S</mi><mo>,</mo><mo>≤</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(S, \leq)</annotation></semantics></math>, an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is <em><a class="existingWikiWord" href="/nlab/show/maximal+element">maximal</a></em> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">y \leq x</annotation></semantics></math> whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \leq y</annotation></semantics></math>.</p> </li> <li> <p>A <em><a class="existingWikiWord" href="/nlab/show/chain">chain</a></em> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/subset">subset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↪</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">A \hookrightarrow S</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/total+order">total order</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>.</p> </li> <li> <p>An <em><a class="existingWikiWord" href="/nlab/show/upper+bound">upper bound</a></em> of a subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">y \leq x</annotation></semantics></math> whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">y \in A</annotation></semantics></math>.</p> </li> </ul> </div> <div class="num_defn" id="statement"> <h6 id="definition_2">Definition</h6> <p>The <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> <strong>Zorn's Lemma</strong> states that a preordered set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> has a maximal element if every chain in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> has an upper bound.</p> </div> <div class="num_theorem" id="TheLemma"> <h6 id="theorem">Theorem</h6> <p>Suppose the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> holds. Then Zorn's Lemma holds.</p> </div> <div class="proof"> <h6 id="proof">Proof</h6> <p>By contradiction. (We freely use the <a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a>, 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 <a class="existingWikiWord" href="/nlab/show/posets">posets</a>.)</p> <p>Suppose <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> has no maximal element. Then every chain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>⊆</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">C \subseteq S</annotation></semantics></math> has a <em>strict</em> upper bound: an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo><</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">c \lt x</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo>∈</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">c \in C</annotation></semantics></math>. (Take an upper bound <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is not maximal by supposition, so any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo><</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">y \lt x</annotation></semantics></math> will serve.) For each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi><mo>⊆</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">W \subseteq S</annotation></semantics></math> that is well-ordered by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math>, use AC to choose a strict upper bound <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>W</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(W)</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>. Given a such a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>Well</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo><mo>→</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">f: Well(S) \to S</annotation></semantics></math> from well-ordered subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>, let us say <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi><mo>∈</mo><mi>Well</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">W \in Well(S)</annotation></semantics></math> is <em><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>-inductive</em> if for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>W</mi></mrow><annotation encoding="application/x-tex">x \in W</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>f</mi><mo stretchy="false">(</mo><mo stretchy="false">{</mo><mi>y</mi><mo>∈</mo><mi>W</mi><mo>:</mo><mi>y</mi><mo><</mo><mi>x</mi><mo stretchy="false">}</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x = f(\{y \in W: y \lt x\})</annotation></semantics></math>.</p> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi><mo>,</mo><mi>Z</mi><mo>∈</mo><mi>Well</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Y, Z \in Well(S)</annotation></semantics></math> be <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>-inductive sets; we will show one is an <a class="existingWikiWord" href="/nlab/show/lower+set">initial segment</a> of the other. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> be the union of all subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> that are initial segments of both <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Z</mi></mrow><annotation encoding="application/x-tex">Z</annotation></semantics></math>; then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> is maximal among such initial segments of both. Suppose <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> is <em>properly</em> contained in both; let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> be the least element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi><mo>∖</mo><mi>I</mi></mrow><annotation encoding="application/x-tex">Y \setminus I</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</annotation></semantics></math> the least element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Z</mi><mo>∖</mo><mi>I</mi></mrow><annotation encoding="application/x-tex">Z \setminus I</annotation></semantics></math>. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>x</mi><mo>∈</mo><mi>Y</mi><mo>:</mo><mi>x</mi><mo><</mo><mi>y</mi><mo stretchy="false">}</mo><mo>=</mo><mi>I</mi><mo>=</mo><mo stretchy="false">{</mo><mi>x</mi><mo>′</mo><mo>∈</mo><mi>Z</mi><mo>:</mo><mi>x</mi><mo>′</mo><mo><</mo><mi>z</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{x \in Y: x \lt y\} = I = \{x' \in Z: x' \lt z\}</annotation></semantics></math>, so by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>-inductivity of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi><mo>,</mo><mi>Z</mi></mrow><annotation encoding="application/x-tex">Y, Z</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>=</mo><mi>f</mi><mo stretchy="false">(</mo><mi>I</mi><mo stretchy="false">)</mo><mo>=</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">y = f(I) = z</annotation></semantics></math>. Thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> extends to an initial segment <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi><mo>∪</mo><mo stretchy="false">{</mo><mi>y</mi><mo stretchy="false">}</mo><mo>=</mo><mi>I</mi><mo>∪</mo><mo stretchy="false">{</mo><mi>z</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">I \cup \{y\} = I \cup \{z\}</annotation></semantics></math>, contradicting maximality of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math>. Therefore we must have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi><mo>=</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">I = Y</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi><mo>=</mo><mi>Z</mi></mrow><annotation encoding="application/x-tex">I = Z</annotation></semantics></math>, so one of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi><mo>,</mo><mi>Z</mi></mrow><annotation encoding="application/x-tex">Y, Z</annotation></semantics></math> is an initial segment of the other.</p> <p>So the collection of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>-inductive sets is totally ordered by inclusion of initial segments, making their union <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> the maximal <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>-inductive set (Lemma <a class="maruku-ref" href="#wo"></a> below). Appending its strict upper bound <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>U</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(U)</annotation></semantics></math>, the chain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>∪</mo><mo stretchy="false">{</mo><mi>f</mi><mo stretchy="false">(</mo><mi>U</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">U \cup \{f(U)\}</annotation></semantics></math> is a larger <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>-inductive set, contradiction. The proof is complete.</p> </div> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>The <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a> (with its unique structure as preordered set) is not an exception to Zorn's lemma, as the chain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\emptyset</annotation></semantics></math> does not have an upper bound.</p> </div> <div class="num_remark"> <h6 id="remark_2">Remark</h6> <p>The proof above (originally by <a href="#Kneser">Kneser</a>) can be seen as an application of general recursion theory à la Paul Taylor’s <a class="existingWikiWord" href="/nlab/show/Practical+Foundations+of+Mathematics">book</a>, which in turn is inspired in large part by <a href="#Osius">Osius</a>. In particular, initial segments are the same as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>-coalgebra maps between <a class="existingWikiWord" href="/nlab/show/well-founded+coalgebras">well-founded coalgebras</a>, and the maximal <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> constructed is a maximal attempt with respect to a partial algebra structure <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>P</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo><mo>⇀</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">f: P(S) \rightharpoonup S</annotation></semantics></math>, 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.</p> </div> <div class="num_lemma" id="wo"> <h6 id="lemma">Lemma</h6> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>P</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">P_\alpha</annotation></semantics></math> be a collection of subsets of a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>, each equipped with a well-ordering <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>≤</mo> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">\leq_\alpha</annotation></semantics></math>, such that for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi><mo>,</mo><mi>β</mi></mrow><annotation encoding="application/x-tex">\alpha, \beta</annotation></semantics></math>, one of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>P</mi> <mi>α</mi></msub><mo>,</mo><msub><mi>P</mi> <mi>β</mi></msub></mrow><annotation encoding="application/x-tex">P_\alpha, P_\beta</annotation></semantics></math> (each with their orderings) is an <a class="existingWikiWord" href="/nlab/show/lower+set">initial segment</a> of the other. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> be the union <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>∪</mo> <mi>α</mi></msub><msub><mi>P</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">\cup_\alpha P_\alpha</annotation></semantics></math>, equipped with the ordering <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \leq y</annotation></semantics></math> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><msub><mo>≤</mo> <mi>α</mi></msub><mi>y</mi></mrow><annotation encoding="application/x-tex">x \leq_\alpha y</annotation></semantics></math> in some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>P</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">P_\alpha</annotation></semantics></math> containing them both. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is well-ordered by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math>, with each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>P</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">P_\alpha</annotation></semantics></math> an initial segment of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>.</p> </div> <div class="proof"> <h6 id="proof_2">Proof</h6> <p>Observe that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> is well-defined, and is a <a class="existingWikiWord" href="/nlab/show/total+order">total order</a>: if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>,</mo><mi>y</mi><mo>∈</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">x, y \in P</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><msub><mi>P</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">x \in P_\alpha</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><msub><mi>P</mi> <mi>β</mi></msub></mrow><annotation encoding="application/x-tex">y \in P_\beta</annotation></semantics></math> for some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi><mo>,</mo><mi>β</mi></mrow><annotation encoding="application/x-tex">\alpha, \beta</annotation></semantics></math>, where one of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>P</mi> <mi>α</mi></msub><mo>,</mo><msub><mi>P</mi> <mi>β</mi></msub></mrow><annotation encoding="application/x-tex">P_\alpha, P_\beta</annotation></semantics></math> contains the other, say <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>P</mi> <mi>α</mi></msub><mo>⊆</mo><msub><mi>P</mi> <mi>β</mi></msub></mrow><annotation encoding="application/x-tex">P_\alpha \subseteq P_\beta</annotation></semantics></math>, whence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>,</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x, y</annotation></semantics></math> are comparable in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>P</mi> <mi>β</mi></msub></mrow><annotation encoding="application/x-tex">P_\beta</annotation></semantics></math>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> is an inhabited subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>∩</mo><msub><mi>P</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">T \cap P_\alpha</annotation></semantics></math> is inhabited for some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>, so there is a minimal element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>∈</mo><mi>T</mi><mo>∩</mo><msub><mi>P</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">t \in T \cap P_\alpha</annotation></semantics></math> with respect to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>≤</mo> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">\leq_\alpha</annotation></semantics></math>. This <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math> is minimal in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> with respect to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math>, for if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>∈</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">s \in T</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>≤</mo><mi>t</mi></mrow><annotation encoding="application/x-tex">s \leq t</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>∈</mo><msub><mi>P</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">s \in P_\alpha</annotation></semantics></math> by the initial segment condition, and then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≤</mo><mi>s</mi></mrow><annotation encoding="application/x-tex">t \leq s</annotation></semantics></math> by definition of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math>.</p> </div> <div class="num_theorem"> <h6 id="theorem_2">Theorem</h6> <p>If Zorn's Lemma and the <a class="existingWikiWord" href="/nlab/show/principle+of+excluded+middle">principle of excluded middle</a> hold, then so do the <a class="existingWikiWord" href="/nlab/show/well-ordering+principle">well-ordering principle</a> and the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>.</p> </div> <div class="proof"> <h6 id="proof_3">Proof</h6> <p>We first show that Zorn’s lemma implies the classical <a class="existingWikiWord" href="/nlab/show/well-ordering+principle">well-ordering principle</a>. The <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> easily follows from the well-ordering principle.</p> <ol> <li> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> be a set, and consider the <a class="existingWikiWord" href="/nlab/show/poset">poset</a> whose elements are pairs <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>R</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(X, R)</annotation></semantics></math>, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>∈</mo><mi>P</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">X \in P A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> is a (classical) <a class="existingWikiWord" href="/nlab/show/well-order">well-order</a>ing on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, ordered by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>R</mi><mo stretchy="false">)</mo><mo>≤</mo><mo stretchy="false">(</mo><mi>Y</mi><mo>,</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(X, R) \leq (Y, S)</annotation></semantics></math> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> as a well-ordered set is an initial segment of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is a chain in the poset consisting of subsets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>X</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">X_\alpha</annotation></semantics></math>, then their union <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is a well-order by Lemma <a class="maruku-ref" href="#wo"></a>, and so the hypothesis of Zorn’s lemma is satisfied.</p> </li> <li> <p>By Zorn’s lemma, conclude that the poset above contains a maximal element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>R</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(X, R)</annotation></semantics></math>, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>⊆</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">X \subseteq A</annotation></semantics></math>. We claim <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>=</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">X = A</annotation></semantics></math>; suppose not (here is where we need <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>), and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> be a member of the complement <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">\neg X</annotation></semantics></math>. Well-order <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>∪</mo><mo stretchy="false">{</mo><mi>x</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">X \cup \{x\}</annotation></semantics></math>, extending <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> by deeming <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to be the final element. This shows <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>R</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(X, R)</annotation></semantics></math> was not maximal, contradiction. Hence any set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> may be well-ordered.</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> follows: suppose given a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>E</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">p: E \to B</annotation></semantics></math>, so that every <a class="existingWikiWord" href="/nlab/show/fiber">fiber</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>p</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p^{-1}(b)</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited</a>. Consider any well-ordering of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math>, and define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">s: B \to E</annotation></semantics></math> by letting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(b)</annotation></semantics></math> be the least element in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>p</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p^{-1}(b)</annotation></semantics></math> with respect to the well-ordering. This gives a section <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math>.</p> </li> </ol> </div> <h2 id="bourbakiwitt_theorem">Bourbaki-Witt theorem</h2> <p>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 <a href="#Bauer">Bauer</a> for a demonstration that it is not valid in the <a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a>. That said, the issue is subtle enough that the Bourbaki-Witt theorem nonetheless holds in topos with a <a class="existingWikiWord" href="/nlab/show/geometric+morphism">geometric morphism</a> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>, for instance any <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a>, assuming B-W holds in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> (<a href="#Bauer-Lumsdaine_13">Bauer-Lumsdaine 2013</a>).</p> <div class="num_theorem"> <h6 id="theorem_3">Theorem</h6> <p><strong>(Bourbaki-Witt)</strong> Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> be an inhabited <a class="existingWikiWord" href="/nlab/show/poset">poset</a> such that every chain has a <a class="existingWikiWord" href="/nlab/show/supremum">least upper bound</a>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>:</mo><mi>P</mi><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">s: P \to P</annotation></semantics></math> a function that is <em>inflationary</em>: satisfies <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>s</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x \leq s(x)</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/fixed+point">fixed point</a>: an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">s(x) = x</annotation></semantics></math>.</p> </div> <div class="proof"> <h6 id="proof_4">Proof</h6> <p>Without loss of generality, assume <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> has a bottom element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math>; otherwise just pick an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">a \in P</annotation></semantics></math> and replace <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> with the upward set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">↑</mo><mi>a</mi></mrow><annotation encoding="application/x-tex">\uparrow a</annotation></semantics></math>.</p> <p>Say that a subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi><mo>⊆</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">I \subseteq P</annotation></semantics></math> is <em><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>-inductive</em> if: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo>∈</mo><mi>I</mi></mrow><annotation encoding="application/x-tex">0 \in I</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> is closed under <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>I</mi><mo stretchy="false">)</mo><mo>⊆</mo><mi>I</mi></mrow><annotation encoding="application/x-tex">s(I) \subseteq I</annotation></semantics></math>), and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> contains the sup of any chain in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math>. The intersection of any family of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>-inductive sets is also <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>-inductive, so the intersection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> of all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>-inductive sets is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>-inductive.</p> <p>The idea is that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> is totally ordered (is a chain) by the following intuition: the elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> are <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo>,</mo><mi>s</mi><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo>,</mo><mi>s</mi><mi>s</mi><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo>,</mo><mi>…</mi><msup><mi>s</mi> <mi>n</mi></msup><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo>,</mo><mi>…</mi></mrow><annotation encoding="application/x-tex">0, s(0), s s(0), \ldots s^n(0), \ldots</annotation></semantics></math>, where we continue by transfinite induction: at limit ordinals <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>s</mi> <mi>α</mi></msup><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s^\alpha(0)</annotation></semantics></math> to be the sup of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><msup><mi>s</mi> <mi>β</mi></msup><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo>:</mo><mi>β</mi><mo><</mo><mi>α</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{s^\beta(0): \beta \lt \alpha\}</annotation></semantics></math>, and at successors define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>s</mi> <mrow><mi>α</mi><mo>+</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><msup><mi>s</mi> <mi>α</mi></msup><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s^{\alpha + 1}(0) = s(s^\alpha(0))</annotation></semantics></math>. We cannot have a strictly increasing chain that goes on forever, by cardinality considerations, so at some point we hit an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>s</mi> <mrow><mi>α</mi><mo>+</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo>=</mo><msup><mi>s</mi> <mi>α</mi></msup><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s^{\alpha + 1}(0) = s^\alpha(0)</annotation></semantics></math>, which provides a fixed point. (What could be nonconstructive about that? See this <a href="https://golem.ph.utexas.edu/category/2012/10/the_zorn_identity.html#c042428">comment</a> by Lumsdaine.) In any case, once we prove <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> is totally ordered, the sup of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> is obviously a fixed point.</p> <p>Without getting into ordinals, one may prove <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> is totally ordered as follows. Call an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo>∈</mo><mi>M</mi></mrow><annotation encoding="application/x-tex">c \in M</annotation></semantics></math> a <em>cap</em> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo><</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">x \lt c</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>M</mi></mrow><annotation encoding="application/x-tex">x\in M</annotation></semantics></math> implies <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">s(x) \leq c</annotation></semantics></math>. For each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo>∈</mo><mi>M</mi></mrow><annotation encoding="application/x-tex">c \in M</annotation></semantics></math>, put <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>c</mi></msub><mo>=</mo><mo stretchy="false">{</mo><mi>x</mi><mo>∈</mo><mi>M</mi><mo>:</mo><mi>x</mi><mo>≤</mo><mi>c</mi><mo>∨</mo><mi>s</mi><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>x</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">M_c = \{x \in M: x \leq c \vee s(c) \leq x\}</annotation></semantics></math>. A routine verification shows <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>c</mi></msub></mrow><annotation encoding="application/x-tex">M_c</annotation></semantics></math> is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>-inductive if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> is a cap, so in fact <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>c</mi></msub><mo>=</mo><mi>M</mi></mrow><annotation encoding="application/x-tex">M_c = M</annotation></semantics></math> by minimality of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math>. Then, show that the set of caps is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>-inductive. This is also routine if we avail ourselves of the just-proven fact that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>M</mi> <mi>c</mi></msub><mo>=</mo><mi>M</mi></mrow><annotation encoding="application/x-tex">M_c = M</annotation></semantics></math> for any cap (but consult Appendix 2 in Lang’s Algebra if you get stuck). So again by minimality of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math>, every element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> is a cap. Finally, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo>,</mo><mi>d</mi><mo>∈</mo><mi>M</mi></mrow><annotation encoding="application/x-tex">c, d \in M</annotation></semantics></math>, use the fact that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> is a cap to conclude either that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>d</mi><mo>≤</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">d \leq c</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">s(c) \leq d</annotation></semantics></math>, whence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo>≤</mo><mi>s</mi><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">c \leq s(c) \leq d</annotation></semantics></math>; thus we see any two elements are comparable.</p> </div> <p>For a discussion of how to get from Bourbaki-Witt to Zorn, see either Lang or this <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-Category Café <a href="https://golem.ph.utexas.edu/category/2012/10/the_zorn_identity.html">post</a> by <a class="existingWikiWord" href="/nlab/show/Tom+Leinster">Tom Leinster</a>, especially the main post which gives three very closely related results bearing on Zorn’s lemma, and a follow-up comment <a href="https://golem.ph.utexas.edu/category/2012/10/the_zorn_identity.html#c042422">here</a> which brings in Bourbaki-Witt.</p> <div class="num_remark"> <h6 id="remark_3">Remark</h6> <p>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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>, consider the function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>Well</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo><mo>→</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">f: Well(S) \to S</annotation></semantics></math> which takes a well-ordered subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>sup</mi><mi>W</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(\sup W)</annotation></semantics></math>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> has no fixed points, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>W</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(W)</annotation></semantics></math> will always be a strict upper bound of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>, and from there one derives a contradiction exactly as in the proof of Zorn’s lemma.</p> </div> <div class="num_remark"> <h6 id="remark_4">Remark</h6> <p>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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> is a monotone operator (preserves the order <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math>) on an inhabited <a class="existingWikiWord" href="/nlab/show/dcpo">dcpo</a>. See <a class="existingWikiWord" href="/nlab/show/fixed+point">fixed point</a> for a brief account, and this <a href="https://topology.lmf.cnrs.fr/bourbaki-witt-and-dito-pataraia/">blog post</a> for some appreciative commentary.</p> </div> <h2 id="wellordered_formulation">Well-ordered formulation</h2> <p><a class="existingWikiWord" href="/nlab/show/Terry+Tao">Terry Tao</a><a href="https://terrytao.wordpress.com/2009/01/28/245b-notes-7-well-ordered-sets-ordinals-and-zorns-lemma-optional/">points out</a> (Remark 14) that the proof of Zorn’s Lemma uses only the well-ordered chains, allowing a weakened hypothesis. This is most naturally stated in the context of <a class="existingWikiWord" href="/nlab/show/quosets">quosets</a> rather than <a class="existingWikiWord" href="/nlab/show/posets">posets</a>:</p> <div class="num_defn" id="WellChainAndStrictUpperBound"> <h6 id="definition_3">Definition</h6> <ul> <li> <p>Given a <a class="existingWikiWord" href="/nlab/show/quasiordered+set">quasiordered set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>S</mi><mo>,</mo><mo><</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(S, \lt)</annotation></semantics></math>, an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is <em><a class="existingWikiWord" href="/nlab/show/maximal+element">maximal</a></em> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo><</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \lt y</annotation></semantics></math> never holds.</p> </li> <li> <p>A <em><a class="existingWikiWord" href="/nlab/show/well-ordered+set">well-ordered</a> chain</em> (or a <em>well-ordered subset</em> or simply a <em>well-chain</em>) in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/subset">subset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↪</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">A \hookrightarrow S</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo><</mo></mrow><annotation encoding="application/x-tex">\lt</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/well+order">well order</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>.</p> </li> <li> <p>A <em><span class="newWikiWord">strict upper bound<a href="/nlab/new/strict+upper+bound">?</a></span></em> of a subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo><</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">y \lt x</annotation></semantics></math> whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">y \in A</annotation></semantics></math>.</p> </li> </ul> </div> <p>The change to <em>strict</em> upper bounds is natural in a quasiordered context; it makes no difference in the presence of excluded middle, since we wish to conclude that a maximal element exists; if there is no maximal element, then any set with an upper bound immediately gets a strict upper bound along with it.</p> <div class="num_defn" id="wellStatement"> <h6 id="definition_4">Definition</h6> <p>The well-ordered <strong>Zorn's Lemma</strong> states that any quasiordered set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> has a maximal element if every well-chain in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> has a strict upper bound, or more simply that it is not possible in a quasiordered set that every well-chain has a strict upper bound. Or from another perspective, if every well-ordered subset of a quasiordered <a class="existingWikiWord" href="/nlab/show/class">class</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> has a strict upper bound, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a>.</p> </div> <p>The ‘more simply’ formulation is equivalent (even constructively) because, on the one hand, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi></mrow><annotation encoding="application/x-tex">m</annotation></semantics></math> is a maximal element, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi></mrow><annotation encoding="application/x-tex">{m}</annotation></semantics></math> is a well-chain with no strict upper bound, contradicting the hypothesis; while on the other hand, anything whatsoever is true of a nonexistent quoset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>. The ‘another perspective’ is then immediate if by a ‘proper class’ one simply means a class that is not a set.</p> <p>Assuming excluded middle, this is (a priori) stronger than the usual Zorn’s Lemma, since only well-ordered chains are required to have upper bounds. (Of course, once all the proofs are in, they are both simply equivalent to the Axiom of Choice.) In <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>, however, it is not stronger, for two reasons: just because <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> has no maximal element, that doesn’t mean that every upper bound has a strict upper bound; and even if this could be fixed, we would only conclude that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> does <a class="existingWikiWord" href="/nlab/show/not+not">not not</a> have a maximal element. However, I intend to argue that this version of Zorn’s Lemma should be regarded as more constructively acceptable; some relativized versions are flat-out true.</p> <h2 id="usageapplications">Usage/applications</h2> <p>It is very common, when starting with a preordered set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>, to apply Zorn's lemma not to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> itself but to an <a class="existingWikiWord" href="/nlab/show/up-set">up-set</a> (an <a class="existingWikiWord" href="/nlab/show/under+category">under category</a>) in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>. That is, one starts with an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> and proves the existence of a maximal element comparable to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>.</p> <p>Zorn's lemma may be used to prove all of the following:</p> <ul> <li>The <a class="existingWikiWord" href="/nlab/show/Hausdorff+maximal+principle">Hausdorff maximal principle</a>: Every chain in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is contained in a maximal chain.</li> <li>The <a class="existingWikiWord" href="/nlab/show/ultrafilter+theorem">ultrafilter theorem</a>: Every proper <a class="existingWikiWord" href="/nlab/show/filter">filter</a> on a set may be extended to an <a class="existingWikiWord" href="/nlab/show/ultrafilter">ultrafilter</a>.</li> <li>The <a class="existingWikiWord" href="/nlab/show/maximal+ideal+theorem">maximal ideal theorem</a>: Every <a class="existingWikiWord" href="/nlab/show/ideal">ideal</a> in a <a class="existingWikiWord" href="/nlab/show/ring">ring</a> may be extended to a <a class="existingWikiWord" href="/nlab/show/maximal+ideal">maximal ideal</a>.</li> <li>The <a class="existingWikiWord" href="/nlab/show/basis+theorem">basis theorem</a>: Every <a class="existingWikiWord" href="/nlab/show/vector+space">vector space</a> (over a <a class="existingWikiWord" href="/nlab/show/field">field</a>) has a basis.</li> <li>etc …</li> </ul> <p>Some of these are equivalent to Zorn's lemma, while some are weaker; conversely, some additionally require excluded middle.</p> <h2 id="references">References</h2> <p>Due Kuratowski and, independently later, Zorn:</p> <ul> <li> <p>Casimir Kuratowski, <em>Une méthode d’élimination des nombres transfinis des raisonnements mathématiques</em>, Fundamenta Mathematicae <strong>3</strong> (1922) 76–108 <a href="https://doi.org/10.4064/fm-3-1-76-108">doi</a></p> </li> <li> <p>Max Zorn, <em>A remark on method in transfinite algebra</em>, Bull. Amer. Math. Soc. <strong>41</strong> (10): 667–670 (1935)<a href="https://doi.org/10.1090/S0002-9904-1935-06166-X">doi</a></p> </li> <li> <p>Serge Lang, <em>Algebra</em> (third edition), Addison-Wesley 1993.</p> </li> <li id="Osius"> <p>Gerhard Osius, <em>Categorical set theory: a characterization of the category of sets</em>, Jour. Pure Appl. Alg. 4 (1974), 79–119. doi:<a href="https://doi.org/10.1016/0022-4049%2874%2990032-2">10.1016/0022-4049(74)90032-2</a></p> </li> <li id="Bauer"> <p><a class="existingWikiWord" href="/nlab/show/Andrej+Bauer">Andrej Bauer</a>, <em>On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos</em>, Electronic Notes in Theoretical Computer Science, <strong>249</strong> (2009) 157–167, doi:<a href="https://doi.org/10.1016/j.entcs.2009.07.089">10.1016/j.entcs.2009.07.089</a> <em>and</em></p> <p>Theoretical Computer Science, <strong>430</strong> (2012) 43–50, doi:<a href="https://doi.org/10.1016/j.tcs.2011.12.005">10.1016/j.tcs.2011.12.005</a>. arXiv:<a href="https://arxiv.org/abs/0911.0068">0911.0068</a>.</p> </li> <li id="Bauer-Lumsdaine_13"> <p><a class="existingWikiWord" href="/nlab/show/Andrej+Bauer">Andrej Bauer</a>, <a class="existingWikiWord" href="/nlab/show/Peter+LeFanu+Lumsdaine">Peter LeFanu Lumsdaine</a>, <em>On the Bourbaki-Witt Principle in Toposes</em>, Math. Proc. Cam. Phil. Soc. 155 (2013), no. 1, 87–99 doi:<a href="https://doi.org/10.1017/S0305004113000108">10.1017/S0305004113000108</a>, arXiv:<a href="https://arxiv.org/abs/1201.0340">1201.0340</a>.</p> </li> <li id="Kneser"> <p>Hellmuth Kneser, <em>Das Auswahlaxiom und das Lemma von Zorn</em>, Mathematische Zeitschrift, 96:62–63, 1967; available <a href="http://resolver.sub.uni-goettingen.de/purl?PPN266833020_0096">here</a></p> </li> </ul> <p>On Zorn’s lemma and <a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean algebra</a> in <a class="existingWikiWord" href="/nlab/show/intuitionistic+type+theories">intuitionistic type theories</a>:</p> <ul> <li id="Bell"><a class="existingWikiWord" href="/nlab/show/John+Lane+Bell">John Lane Bell</a>, <em>Zorn’s lemma and complete Boolean algebras in intuitionistic type theories</em>, The Journal of Symbolic Logic, 62(4):1265–1279, 1997 (<a href="https://doi.org/10.2307/2275642">doi:10.2307/2275642</a>)</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on May 9, 2024 at 12:05:41. See the <a href="/nlab/history/Zorn%27s+lemma" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/Zorn%27s+lemma" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4303/#Item_7">Discuss</a><span class="backintime"><a href="/nlab/revision/Zorn%27s+lemma/29" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/Zorn%27s+lemma" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/Zorn%27s+lemma" accesskey="S" class="navlink" id="history" rel="nofollow">History (29 revisions)</a> <a href="/nlab/show/Zorn%27s+lemma/cite" style="color: black">Cite</a> <a href="/nlab/print/Zorn%27s+lemma" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/Zorn%27s+lemma" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>