Editing Axiom of choice (section)

==Usage==
Until the late 19th century, the axiom of choice was often used implicitly, although it had not yet been formally stated. For example, after having established that the set ''X'' contains only non-empty sets, a mathematician might have said "let ''F''(''s'') be one of the members of ''s'' for all ''s'' in ''X''" to define a function ''F''.  In general, it is impossible to prove that ''F'' exists without the axiom of choice, but this seems to have gone unnoticed until [[Zermelo]].
<!--Not every situation requires the full axiom of choice. For a finite collection of sets ''X'', the axiom of choice follows from the other axioms of set theory. In that case, it is equivalent to saying that if we have several (a finite number of) boxes, each containing at least one item, then we can choose exactly one item from each box. Clearly, we can do this with the principle of finite induction: We start at the first box, choose an item; go to the second box, choose an item; and so on. The number of boxes is finite, so induction guarantees that our choice procedure is well-defined and eventually terminates. The result is an explicit choice function: a function that takes the first box to the first element we chose, the second box to the second element we chose, and so on. This shows that the axiom of choice restricted to finite sets (i.e., the statement "for every natural number ''k'', every family of ''k'' nonempty sets has a choice function") is a direct consequence of the axiom of finite induction and does not need anything beyond ZF. However, this argument will not work if the collection of sets ''X'' is infinite. For example, to show that every infinite sequence of nonempty sets has a choice function, as is asserted by the [[axiom of countable choice]], one needs to go beyond finite induction to countably transfinite induction. If the above method is applied to an infinite sequence (''X''<sub>''i''</sub> : ''i''∈ω) of nonempty sets, a function is obtained at each finite stage, but there is no stage at which a choice function for the entire family is constructed, and no "limiting" choice function can be constructed, in general (within ZF). Countable transfinite induction (a.k.a. the [[axiom of dependent choice]]) essentially guarantees the existence of such a "limiting" choice function, and thus implies the axiom of countable choice. It is however weaker than the full axiom of choice.--> <!--This whole section needs rewriting; it says something kind of true, but equates choice with induction, which is wrong.  Choice is induction plus choosing.  -->