The axiom of countable choice (), also called or , 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.) All the reasoning in this page is constructive.
More explicitly, let be any set and let be a surjection. Then the axiom of countable choice states that has a section. If you phrase the axiom of choice in terms of entire relations, then countable choice states that any entire relation from to any other set contains (in the 2-poset Rel) a functional entire relation.
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 , is the axiom of dependent choice (). In general, is enough to justify results in analysis involving sequences.
Sometimes in foundations it is useful to consider a weaker version of countable choice, called . This states that any entire relation from to itself contains a functional entire relation. In terms of surjections, this states that any surjection has a section if is a subset of and is the restriction to of a product projection. is enough to prove that every Dedekind real number is a Cauchy real number (the converse is always true).
The axiom of weak countable choice () states that a surjection has a section if, whenever , at least one of the preimages and is a singleton. follows (for different reasons) from either or excluded middle. On the other hand, 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).
An even weaker form of countable choice was proposed by Martin Escardo; it states that any surjection of the form has a section, where is a decidable subset and is an arbitrary set with the projection. This follows from WCC and also from the limited principle of omniscience; see the constructivenews discussion.
Martin Escardo et. al., Special case of countable choice, message and discussion to the constructivenews list, google groups