nLab countable choice

Countable choice




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Countable choice


The axiom of countable choice (CCCC), also called AC ωAC_\omega or AC NAC_N, is a weak form of the axiom of choice; it says that the set of natural numbers is a projective object in Set. (Recall that the full axiom of choice states that every set is projective.)

In classical mathematics, countable choice is usually accepted because the full axiom of choice is accepted. In constructive mathematics 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 internal logic 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. Fred Richman (RichmanFTA) has said that

Countable choice is a blind spot for constructive mathematicians in much the same way as excluded middle is for classical mathematicians.

All the reasoning in this page is constructive.


In set theory

More explicitly, let XX be any set and let p:XNp\colon X \to \mathbf{N} be a surjection. Then the axiom of countable choice states that pp has a section. If you phrase the axiom of choice in terms of entire relations, then countable choice states that any entire relation from N\mathbf{N} to any other set contains (in the 2-poset Rel) a functional entire relation.

In dependent type theory

In dependent type theory, countable choice says that the dependent product of a family of inhabited sets indexed by the natural numbers is itself inhabited:

Γ,n:A(n)typeΓAC A:( n:isSet(A(n)))( n:[A(n)])[ n:A(n)]\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]}

Alternatively, the axiom of countable choice states that given a family of sets A(n)A(n) indexed by natural numbers nn and a family of propositions P(n,x)P(n, x) indexed by natural numbers nn and element x:A(n)x:A(n), if for all natural numbers nn there merely exists an element x:A(n)x:A(n) such that P(n,x)P(n, x), then there merely exists a dependent function g: n:A(n)g:\prod_{n:\mathbb{N}} A(n) such that for all natural numbers nn, P(n,g(n))P(n, g(n)):

Γ,n:A(n)typeΓ,n:,x:A(n)P(n,x)typeΓAC A,P:( n:isSet(A(n))× x:A(n)isProp(P(n,x)))( n:x:A(n).P(n,x))g: n:A(n). n:P(n,g(n))\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))}


Here we collect some consequences of the countable axiom of choice.



Unlike the full axiom of choice, countable choice is often considered to be a constructively acceptable principle. In particular, it does not imply the principle of excluded middle. It is a consequence of COSHEP. A stronger version of countable choice, also a consequence of COSHEPCOSHEP, is the axiom of dependent choice (DCDC). In general, DCDC is enough to justify results in analysis involving sequences.

AC 00AC_{00}

Sometimes in foundations it is useful to consider a weaker version of countable choice, called AC 00AC_{00}. This states that any entire relation from N\mathbf{N} to itself contains a functional entire relation. In terms of surjections, this states that any surjection p:XNp\colon X \to \mathbf{N} has a section if XX is a subset of N×N\mathbf{N} \times \mathbf{N} and pp is the restriction to XX of a product projection. AC 00AC_{00} is enough to prove that every Dedekind real number is a Cauchy real number (the converse is always true).

Weak countable choice

The axiom of weak countable choice (WCCWCC) states that a surjection p:XNp\colon X \to \mathbf{N} has a section if, whenever mnm \neq n, at least one of the preimages p *(m)p^*(m) and p *(n)p^*(n) is a singleton. WCCWCC follows (for different reasons) from either CCCC or excluded middle. On the other hand, WCCWCC is enough to prove that the fundamental theorem of algebra in the sense that every non-constant complex polynomial has a root; see Bridges et al (1998).

Another weak countable choice

An axiom variously called AC weakAC_{weak} and AC N2AC_{N2} is countable choice for subsets of {0,1}\{0,1\}; that is, every \mathbb{N}-indexed sequence of inhabited subsets of {0,1}\{0,1\} has a choice function. Like WCCWCC above, this also follows from either CCCC or excluded middle. It is enough to prove the equivalence of the Dedekind reals and Cauchy reals. See Saving et al (2021).

Very weak countable choice

An even weaker form of countable choice was proposed by Martin Escardo; it states that any surjection of the form A(N×B)NA \sqcup (\mathbf{N}\times B) \to \mathbf{N} has a section, where ANA\to \mathbf{N} is a decidable subset and BB is an arbitrary set with N×BN\mathbf{N}\times B \to \mathbf{N} the projection. This follows from WCC and also from the limited principle of omniscience; see the constructivenews discussion.

Topos violating the CAC

One easy example is the category Sh([0,1])Sh([0,1]), the sheaves on the unit interval, since in that topos the Dedekind real numbers and the Cauchy real numbers are not isomorphic, and this is a consequence of the internal countable choice.

Discussion here.

In higher category theory

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 effective epimorphism in an (infinity,1)-category or a related notion such as eso morphisms.

There are multiple version of the axiom of countable choice, depending on what truncation requirements, if any, are applied to the domain.

  • An (,1)(\infty,1)-category satisfies the axiom of countable nn-choice, or CC nCC_n, if every nn-truncated morphism? into the natural numbers object has a section. We write CC CC_\infty for the axiom of countable infinity-choice: the statement that every morphism with codomain the natural numbers object has a section.

These are stronger axioms as nn increases.

There are also “internal” versions of these axioms.

  • In homotopy type theory (the internal logic of an (,1)(\infty,1)-topos), the internal version of CC nCC_n is “every surjection onto the natural numbers type with nn-type fibers has a section”, or equivalently

    (Y:nType)( (x:)Y(x) (x:)Y(x))\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)
  • More generally, we can replace the (1)(-1)-truncation by the kk-truncation to obtain a family of axioms CC k,nCC_{k,n}.

  • We can also replace the (1)(-1)-truncation by the assertion of kk-connectedness, obtaining the axiom of countable kk-connected choice.


See also

Last revised on March 18, 2024 at 10:59:37. See the history of this page for a list of all contributions to it.