Source : Free On-Line Dictionary of Computing

Axiom of Choice
     
         (AC, or "Choice") An {axiom} of {set theory}:
     
        If X is a set of sets, and S is the union of all the elements
        of X, then there exists a function f:X -> S such that for all
        non-empty x in X, f(x) is an element of x.
     
        In other words, we can always choose an element from each set
        in a set of sets, simultaneously.
     
        Function f is a "choice function" for X - for each x in X, it
        chooses an element of x.
     
        Most people's reaction to AC is: "But of course that's true!
        From each set, just take the element that's biggest,
        stupidest, closest to the North Pole, or whatever".  Indeed,
        for any {finite} set of sets, we can simply consider each set
        in turn and pick an arbitrary element in some such way.  We
        can also construct a choice function for most simple {infinite
        sets} of sets if they are generated in some regular way.
        However, there are some infinite sets for which the
        construction or specification of such a choice function would
        never end because we would have to consider an infinite number
        of separate cases.
     
        For example, if we express the {real number} line R as the
        union of many "copies" of the {rational numbers}, Q, namely Q,
        Q+a, Q+b, and infinitely (in fact uncountably) many more,
        where a, b, etc. are {irrational numbers} no two of which
        differ by a rational, and
     
          Q+a == {q+a : q in Q}
     
        we cannot pick an element of each of these "copies" without
        AC.
     
        An example of the use of AC is the theorem which states that
        the {countable} union of countable sets is countable.  I.e. if
        X is countable and every element of X is countable (including
        the possibility that they're finite), then the sumset of X is
        countable.  AC is required for this to be true in general.
     
        Even if one accepts the axiom, it doesn't tell you how to
        construct a choice function, only that one exists.  Most
        mathematicians are quite happy to use AC if they need it, but
        those who are careful will, at least, draw attention to the
        fact that they have used it.  There is something a little odd
        about Choice, and it has some alarming consequences, so
        results which actually "need" it are somehow a bit suspicious,
        e.g. the {Banach-Tarski paradox}.  On the other side, consider
        {Russell's Attic}.
     
        AC is not a {theorem} of {Zermelo Frankel set theory} (ZF).
        Godel and Paul Cohen proved that AC is independent of ZF,
        i.e. if ZF is consistent, then so are ZFC (ZF with AC) and
        ZF(~C) (ZF with the negation of AC).  This means that we
        cannot use ZF to prove or disprove AC.
     
        (2003-07-11)