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> countable choice 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> countable choice </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/15405/#Item_5" 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>Countable choice</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+inequality+spaces">axiom of inequality spaces</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="countable_choice">Countable choice</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#definition'>Definition</a></li> <ul> <li><a href='#in_set_theory'>In set theory</a></li> <li><a href='#in_dependent_type_theory'>In dependent type theory</a></li> </ul> <li><a href='#consequences'>Consequences</a></li> <li><a href='#variations'>Variations</a></li> <ul> <li><a href='#__'><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>COSHEP</mi></mrow><annotation encoding="application/x-tex">COSHEP</annotation></semantics></math> & <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>DC</mi></mrow><annotation encoding="application/x-tex">DC</annotation></semantics></math></a></li> <li><a href='#'><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>AC</mi> <mn>00</mn></msub></mrow><annotation encoding="application/x-tex">AC_{00}</annotation></semantics></math></a></li> <li><a href='#WCC'>Weak countable choice</a></li> <li><a href='#ACN2'>Another weak countable choice</a></li> <li><a href='#very_weak_countable_choice'>Very weak countable choice</a></li> <li><a href='#topos_violating_the_cac'>Topos violating the CAC</a></li> <li><a href='#in_higher_category_theory'>In higher category theory</a></li> </ul> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>The axiom of <strong>countable choice</strong> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>CC</mi></mrow><annotation encoding="application/x-tex">CC</annotation></semantics></math>), also called <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>AC</mi> <mi>ω</mi></msub></mrow><annotation encoding="application/x-tex">AC_\omega</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>AC</mi> <mi>N</mi></msub></mrow><annotation encoding="application/x-tex">AC_N</annotation></semantics></math>, is a weak form of the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>; it says that the set of <a class="existingWikiWord" href="/nlab/show/natural+number">natural number</a>s is a <a class="existingWikiWord" href="/nlab/show/projective+object">projective object</a> in <a class="existingWikiWord" href="/nlab/show/Set">Set</a>. (Recall that the full axiom of choice states that <em>every</em> set is projective.)</p> <p>In <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>, countable choice is usually accepted because the full axiom of choice is accepted. In <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a> the situation is more subtle. For varying reasons, some schools of constructive mathematics accept countable choice (though they reject the full axiom of choice). On the other hand, countable choice is not valid in the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> of a general topos, so if one desires this level of generality then it should not be assumed. There are also philosophical constructivist arguments against it. <a class="existingWikiWord" href="/nlab/show/Fred+Richman">Fred Richman</a> <a href="#RichmanFTA">(RichmanFTA)</a> has said that</p> <blockquote> <p>Countable choice is a blind spot for constructive mathematicians in much the same way as excluded middle is for classical mathematicians.</p> </blockquote> <p>All the reasoning in this page is <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive</a>.</p> <h2 id="definition">Definition</h2> <h3 id="in_set_theory">In set theory</h3> <p>More explicitly, 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 any <a class="existingWikiWord" href="/nlab/show/set">set</a> and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">p\colon X \to \mathbf{N}</annotation></semantics></math> be a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a>. Then the axiom of countable choice states that <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 <a class="existingWikiWord" href="/nlab/show/section">section</a>. If you phrase the axiom of choice in terms of <a class="existingWikiWord" href="/nlab/show/entire+relations">entire relations</a>, then countable choice states that any entire relation from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{N}</annotation></semantics></math> to any other set contains (in the <a class="existingWikiWord" href="/nlab/show/2-poset">2-poset</a> <a class="existingWikiWord" href="/nlab/show/Rel">Rel</a>) a <a class="existingWikiWord" href="/nlab/show/functional+relation">functional</a> entire relation.</p> <h3 id="in_dependent_type_theory">In dependent type theory</h3> <p>In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, <strong>countable choice</strong> says that the <a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product</a> of a family of inhabited sets indexed by the <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a> is itself inhabited:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msubsup><mi mathvariant="normal">AC</mi> <mi>ℕ</mi> <mi>A</mi></msubsup><mo>:</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></munder><mi mathvariant="normal">isSet</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>)</mo></mrow><mo>→</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></munder><mo stretchy="false">[</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo><mo>)</mo></mrow><mo>→</mo><mrow><mo>[</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></munder><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>]</mo></mrow></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma \vdash \mathrm{AC}_\mathbb{N}^A:\left(\prod_{n:\mathbb{N}} \mathrm{isSet}(A(n))\right) \to \left(\prod_{n:\mathbb{N}} [A(n)]\right) \to \left[\prod_{n:\mathbb{N}} A(n)\right]}</annotation></semantics></math></div> <p>Alternatively, the axiom of countable choice states that given a family of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A(n)</annotation></semantics></math> indexed by natural numbers <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> and a family of propositions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(n, x)</annotation></semantics></math> indexed by natural numbers <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> and element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A(n)</annotation></semantics></math>, if for all natural numbers <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> there merely exists an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A(n)</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(n, x)</annotation></semantics></math>, then there merely exists a dependent function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>:</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></msub><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g:\prod_{n:\mathbb{N}} A(n)</annotation></semantics></math> such that for all natural numbers <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>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mi>g</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(n, g(n))</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msubsup><mi mathvariant="normal">AC</mi> <mi>ℕ</mi> <mrow><mi>A</mi><mo>,</mo><mi>P</mi></mrow></msubsup><mo>:</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></munder><mi mathvariant="normal">isSet</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>×</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></munder><mi mathvariant="normal">isProp</mi><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>)</mo></mrow><mo>→</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></munder><mo>∃</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>.</mo><mi>P</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>)</mo></mrow><mo>→</mo><mo>∃</mo><mi>g</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></munder><mi>A</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>.</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></munder><mi>P</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mi>g</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type} \quad \Gamma, n:\mathbb{N}, x:A(n) \vdash P(n, x) \; \mathrm{type}}{\Gamma \vdash \mathrm{AC}_\mathbb{N}^{A, P}:\left(\prod_{n:\mathbb{N}} \mathrm{isSet}(A(n)) \times \prod_{x:A(n)} \mathrm{isProp}(P(n, x))\right) \to \left(\prod_{n:\mathbb{N}} \exists x:A(n).P(n, x)\right) \to \exists g:\prod_{n:\mathbb{N}} A(n).\prod_{n:\mathbb{N}} P(n, g(n))}</annotation></semantics></math></div> <h2 id="consequences">Consequences</h2> <p>Here we collect some consequences of the countable axiom of choice.</p> <ul> <li> <p>The <a class="existingWikiWord" href="/nlab/show/Cauchy+real+numbers">Cauchy real numbers</a> and <a class="existingWikiWord" href="/nlab/show/Dedekind+real+numbers">Dedekind real numbers</a> coincide (the <a class="existingWikiWord" href="/nlab/show/law+of+excluded+middle">law of excluded middle</a> also separately implies this).</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/Rosolini+dominance">Rosolini dominance</a> is a <a class="existingWikiWord" href="/nlab/show/dominance">dominance</a> (the <a class="existingWikiWord" href="/nlab/show/law+of+excluded+middle">law of excluded middle</a> also separately implies this).</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/countable+unions+of+countable+sets+are+countable">countable unions of countable sets are countable</a></p> </li> </ul> <h2 id="variations">Variations</h2> <h3 id="__"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>COSHEP</mi></mrow><annotation encoding="application/x-tex">COSHEP</annotation></semantics></math> & <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>DC</mi></mrow><annotation encoding="application/x-tex">DC</annotation></semantics></math></h3> <p>Unlike the full axiom of choice, countable choice is often considered to be a <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructively</a> acceptable principle. In particular, it does not imply the principle of <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>. It is a consequence of <a class="existingWikiWord" href="/nlab/show/COSHEP">COSHEP</a>. A stronger version of countable choice, also a consequence of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>COSHEP</mi></mrow><annotation encoding="application/x-tex">COSHEP</annotation></semantics></math>, is the axiom of <a class="existingWikiWord" href="/nlab/show/dependent+choice">dependent choice</a> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>DC</mi></mrow><annotation encoding="application/x-tex">DC</annotation></semantics></math>). In general, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>DC</mi></mrow><annotation encoding="application/x-tex">DC</annotation></semantics></math> is enough to justify results in <a class="existingWikiWord" href="/nlab/show/analysis">analysis</a> involving <a class="existingWikiWord" href="/nlab/show/sequences">sequences</a>.</p> <h3 id=""><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>AC</mi> <mn>00</mn></msub></mrow><annotation encoding="application/x-tex">AC_{00}</annotation></semantics></math></h3> <p>Sometimes in foundations it is useful to consider a weaker version of countable choice, called <strong><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>AC</mi> <mn>00</mn></msub></mrow><annotation encoding="application/x-tex">AC_{00}</annotation></semantics></math></strong>. This states that any entire relation from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{N}</annotation></semantics></math> to itself contains a functional entire relation. In terms of surjections, this states that any surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">p\colon X \to \mathbf{N}</annotation></semantics></math> has a section 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> is a <a class="existingWikiWord" href="/nlab/show/subset">subset</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>N</mi></mstyle><mo>×</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{N} \times \mathbf{N}</annotation></semantics></math> and <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 the <a class="existingWikiWord" href="/nlab/show/restriction">restriction</a> 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> of a product projection. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>AC</mi> <mn>00</mn></msub></mrow><annotation encoding="application/x-tex">AC_{00}</annotation></semantics></math> is enough to prove that every <a class="existingWikiWord" href="/nlab/show/Dedekind+real+number">Dedekind real number</a> is a <a class="existingWikiWord" href="/nlab/show/Cauchy+real+number">Cauchy real number</a> (the converse is always true).</p> <h3 id="WCC">Weak countable choice</h3> <p>The axiom of <strong>weak countable choice</strong> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>WCC</mi></mrow><annotation encoding="application/x-tex">WCC</annotation></semantics></math>) states that a surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">p\colon X \to \mathbf{N}</annotation></semantics></math> has a section if, whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>≠</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m \neq n</annotation></semantics></math>, at least one of the <a class="existingWikiWord" href="/nlab/show/preimages">preimages</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>p</mi> <mo>*</mo></msup><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p^*(m)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>p</mi> <mo>*</mo></msup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p^*(n)</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/singleton">singleton</a>. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>WCC</mi></mrow><annotation encoding="application/x-tex">WCC</annotation></semantics></math> follows (for different reasons) from either <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>CC</mi></mrow><annotation encoding="application/x-tex">CC</annotation></semantics></math> or <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>. On the other hand, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>WCC</mi></mrow><annotation encoding="application/x-tex">WCC</annotation></semantics></math> is enough to prove that the <a class="existingWikiWord" href="/nlab/show/fundamental+theorem+of+algebra">fundamental theorem of algebra</a> in the sense that every non-constant complex polynomial has a root; see <a href="#BRS">Bridges et al (1998)</a>. It is an open question whether <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>WCC</mi></mrow><annotation encoding="application/x-tex">WCC</annotation></semantics></math> implies that the <a class="existingWikiWord" href="/nlab/show/Dedekind+reals">Dedekind reals</a> and <a class="existingWikiWord" href="/nlab/show/Cauchy+reals">Cauchy reals</a> coincide, see <a href="#King2024">King et al (2024)</a>.</p> <h3 id="ACN2">Another weak countable choice</h3> <p>An axiom variously called <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>AC</mi> <mi>weak</mi></msub></mrow><annotation encoding="application/x-tex">AC_{weak}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>AC</mi> <mrow><mi>N</mi><mn>2</mn></mrow></msub></mrow><annotation encoding="application/x-tex">AC_{N2}</annotation></semantics></math> is countable choice for subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{0,1\}</annotation></semantics></math>; that is, every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math>-indexed sequence of inhabited subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{0,1\}</annotation></semantics></math> has a choice function. Like <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>WCC</mi></mrow><annotation encoding="application/x-tex">WCC</annotation></semantics></math> above, this also follows from either <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>CC</mi></mrow><annotation encoding="application/x-tex">CC</annotation></semantics></math> or excluded middle. It is enough to prove the equivalence of the <a class="existingWikiWord" href="/nlab/show/Dedekind+reals">Dedekind reals</a> and <a class="existingWikiWord" href="/nlab/show/Cauchy+reals">Cauchy reals</a>. See <a href="#Saving2021">Saving et al (2021)</a>, <a href="#King2024">King et al (2024)</a>.</p> <h3 id="very_weak_countable_choice">Very weak countable choice</h3> <p>An even weaker form of countable choice was proposed by <a href="#EscardoCN">Martin Escardo</a>; it states that any surjection of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊔</mo><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle><mo>×</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">A \sqcup (\mathbf{N}\times B) \to \mathbf{N}</annotation></semantics></math> has a section, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>→</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">A\to \mathbf{N}</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/decidable+subset">decidable subset</a> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> is an arbitrary set with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>N</mi></mstyle><mo>×</mo><mi>B</mi><mo>→</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{N}\times B \to \mathbf{N}</annotation></semantics></math> the projection. This follows from WCC and also from the <a class="existingWikiWord" href="/nlab/show/limited+principle+of+omniscience">limited principle of omniscience</a>; see the <a href="#EscardoCN">constructivenews discussion</a>.</p> <h3 id="topos_violating_the_cac">Topos violating the CAC</h3> <p>One easy example is the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mo stretchy="false">[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">]</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sh([0,1])</annotation></semantics></math>, the sheaves on the unit interval, since in that topos the <a class="existingWikiWord" href="/nlab/show/real+numbers+object#classical_dedekind_real_numbers">Dedekind real numbers</a> and the <a class="existingWikiWord" href="/nlab/show/real+numbers+object#cauchy_real_numbers">Cauchy real numbers</a> are not isomorphic, and this is a consequence of the internal countable choice.</p> <p>Discussion <a href="https://mathoverflow.net/questions/79807/example-of-a-topos-that-violates-countable-choice">here</a>.</p> <h3 id="in_higher_category_theory">In higher category theory</h3> <p>To formulate a version of the axiom of countable choice in a higher category, one has to make an appropriate choice of the meaning of “epimorphism”. In most cases, it is best to choose <a class="existingWikiWord" href="/nlab/show/effective+epimorphisms">effective epimorphism in an (infinity,1)-category</a> or a related notion such as <a class="existingWikiWord" href="/nlab/show/eso+morphisms">eso morphisms</a>.</p> <p>There are multiple version of the axiom of countable choice, depending on what <a class="existingWikiWord" href="/nlab/show/truncated+object">truncation</a> requirements, if any, are applied to the domain.</p> <ul> <li>An <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>∞</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\infty,1)</annotation></semantics></math>-category satisfies the <strong>axiom of countable <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>-choice</strong>, or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>CC</mi> <mi>n</mi></msub></mrow><annotation encoding="application/x-tex">CC_n</annotation></semantics></math>, if every <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>-<span class="newWikiWord">truncated morphism<a href="/nlab/new/truncated+morphism">?</a></span> into the <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a> has a section. We write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>CC</mi> <mn>∞</mn></msub></mrow><annotation encoding="application/x-tex">CC_\infty</annotation></semantics></math> for the <strong>axiom of countable infinity-choice</strong>: the statement that <em>every</em> morphism with codomain the <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a> has a section.</li> </ul> <p>These are stronger axioms as <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> increases.</p> <p>There are also “internal” versions of these axioms.</p> <ul> <li> <p>In <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> (the internal logic of an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>∞</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\infty,1)</annotation></semantics></math>-topos), the internal version of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>CC</mi> <mi>n</mi></msub></mrow><annotation encoding="application/x-tex">CC_n</annotation></semantics></math> is “every surjection onto the natural numbers type with <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>-type fibers has a section”, or equivalently</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mo stretchy="false">(</mo><mi>Y</mi><mo>:</mo><mi>ℕ</mi><mo>→</mo><mi>n</mi><mi>Type</mi><mo stretchy="false">)</mo></mrow></munder><mo maxsize="1.8em" minsize="1.8em">(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mo stretchy="false">(</mo><mi>x</mi><mo>:</mo><mi>ℕ</mi><mo stretchy="false">)</mo></mrow></munder><mo stretchy="false">‖</mo><mi>Y</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">‖</mo><mo>→</mo><mo maxsize="1.8em" minsize="1.8em">‖</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mo stretchy="false">(</mo><mi>x</mi><mo>:</mo><mi>ℕ</mi><mo stretchy="false">)</mo></mrow></munder><mi>Y</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo maxsize="1.8em" minsize="1.8em">‖</mo><mo maxsize="1.8em" minsize="1.8em">)</mo></mrow><annotation encoding="application/x-tex">\prod_{(Y:\mathbb{N}\to n Type)} \Big( \prod_{(x:\mathbb{N})} \Vert Y(x)\Vert \to \Big\Vert \prod_{(x:\mathbb{N})} Y(x) \Big\Vert \Big) </annotation></semantics></math></div></li> <li> <p>More generally, we can replace the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-1)</annotation></semantics></math>-truncation by the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi></mrow><annotation encoding="application/x-tex">k</annotation></semantics></math>-truncation to obtain a family of axioms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>CC</mi> <mrow><mi>k</mi><mo>,</mo><mi>n</mi></mrow></msub></mrow><annotation encoding="application/x-tex">CC_{k,n}</annotation></semantics></math>.</p> </li> <li> <p>We can also replace the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-1)</annotation></semantics></math>-truncation by the assertion of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi></mrow><annotation encoding="application/x-tex">k</annotation></semantics></math>-connectedness, obtaining the <strong>axiom of countable <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi></mrow><annotation encoding="application/x-tex">k</annotation></semantics></math>-connected choice</strong>.</p> </li> </ul> <h2 id="references">References</h2> <ul> <li id="BRS"> <p><a class="existingWikiWord" href="/nlab/show/Fred+Richman">Fred Richman</a>, <a class="existingWikiWord" href="/nlab/show/Douglas+Bridges">Douglas Bridges</a>, Peter Schuster, <em>A weak countable choice principle</em>. Proceedings of the American Mathematical Society 128(9):2749-2752, March 2000. [<a href="http://dx.doi.org/10.1090/S0002-9939-00-05327-2">doi:10.1090/S0002-9939-00-05327-2</a>]</p> </li> <li id="EscardoCN"> <p><a class="existingWikiWord" href="/nlab/show/Martin+Escardo">Martin Escardo</a> et. al., <em>Special case of countable choice</em>, message and discussion to the constructivenews list, <a href="https://groups.google.com/d/msg/constructivenews/PeLsQWDFJNg/7piOmUHbAAAJ">google groups</a></p> </li> <li id="RichmanFTA"> <p><a class="existingWikiWord" href="/nlab/show/Fred+Richman">Fred Richman</a>, <em>The fundamental theorem of algebra: a constructive development without choice</em>. Pacific Journal of Mathematics <strong>196</strong> 1 (2000) 213–230 [<a href="http://dx.doi.org/10.2140/pjm.2000.196.213">doi:10.2140/pjm.2000.196.213</a>, <a href="https://msp.org/pjm/2000/196-1/pjm-v196-n1-p10-p.pdf">pdf</a>]</p> </li> <li id="Saving2021"> <p>Mark Saving et al (2021). <em>A weak form of countable choice</em>. <a href="https://mathoverflow.net/questions/385805/a-weak-form-of-countable-choice/">MathOverflow</a>.</p> </li> <li id="King2024"> <p>Christopher King et al (2024). <em>Does weak countable choice imply that the Cauchy reals are Dedekind complete?</em> <a href="https://mathoverflow.net/questions/461200/does-weak-countable-choice-imply-that-the-cauchy-reals-are-dedekind-complete">MathOverflow</a>.</p> </li> </ul> <p>See also</p> <ul> <li>Wikipedia, <em><a href="https://en.wikipedia.org/wiki/Axiom_of_countable_choice">Axiom of countable choice</a></em></li> </ul> <div class="property">category: <a class="category_link" href="/nlab/all_pages/foundational+axiom">foundational axiom</a></div></body></html> </div> <div class="revisedby"> <p> Last revised on July 5, 2024 at 16:29:07. See the <a href="/nlab/history/countable+choice" 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/countable+choice" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/15405/#Item_5">Discuss</a><span class="backintime"><a href="/nlab/revision/countable+choice/30" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/countable+choice" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/countable+choice" accesskey="S" class="navlink" id="history" rel="nofollow">History (30 revisions)</a> <a href="/nlab/show/countable+choice/cite" style="color: black">Cite</a> <a href="/nlab/print/countable+choice" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/countable+choice" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>