are countable: As pointed out above, to show that a countable union of countable sets is itself countable requires the Axiom of countable choice. There is a field with no algebraic closure. In all models of ZF¬C there is a vector space with no basis. There is a vector space with two bases of different cardinalities. There is a free complete boolean algebra on countably many generators. There is a set that cannot be linearly ordered. There exists a model of ZF¬C in which every set in Rn is measurable. Thus it is possible to exclude counterintuitive results like the Banach–Tarski paradox which are provable in ZFC. Furthermore, this is possible whilst assuming the Axiom of dependent choice, which is weaker than AC but sufficient to develop most of real analysis. In all models of ZF¬C, the generalized continuum hypothesis does not hold. For proofs, see . Additionally, by imposing definability conditions on sets (in the sense of descriptive set theory) one can often prove restricted versions of the axiom of choice from axioms incompatible with general choice. This appears, for example, in the Moschovakis coding lemma. Axiom of choice in type theory In type theory, a different kind of statement is known as the axiom of choice. This form begins with two types, σ and τ, and a relation R between objects of type σ and objects of type τ. The axiom of choice states that if for each x of type σ there exists a y of type τ such that R(x,y), then there is a function f from objects of type σ to objects of type τ such that R(x,f(x)) holds for all x of type σ: Unlike in set theory, the axiom of choice in type theory is typically stated as an axiom scheme, in which R varies over all formulas or over all formulas of a particular logical form. Quotations This is a joke: although the three are all mathematically equivalent, many mathematicians find the axiom of choice to be intuitive, the well-ordering principle to be counterintuitive, and Zorn's lemma to be too complex for any intuition. The observation here is that one can define a function to select from an infinite number of pairs of shoes, for example by choosing the left shoe from each pair. Without the axiom of choice, one cannot assert that such a function exists for pairs of socks, because