Conference rusure::math

> Evident difficulties in naming (building) an element arise in measure-based
> sets (e.g. of the "almost everywhere" type). Can you think about other
> examples?
    
    Say "the set of all everywhere-continuous, nowhere-differentiable 
    	functions from R onto R".

  (AC) A direct product of non-empty sets is non-empty.

More exactly, the direct product of a `small' family of non-empty sets
(indexed by a set) is non-empty. 

  (WAC) Consider a non-empty set. Then we can choose an element of this set.

I looked in "Sets: an introduction" by Michael Potter, and where the axiom
of choice is defined to say that every set has a choice function: a function
f defined on its non-empty elements whose value at such an argument is
an element of the argument.  He proves this equivalent to the axiom above.
The only other plausible interpretation of WAC is what Potter calls the
axiom of global choice, which asserts that there's one choice function
which does for all sets, which isn't weak!

   Should we feel free to use it? (We actually do).   

We should.  Arguments which make *essential* use of it are found only 
in the most abstract parts of mathematics.  

Hank

PS: Potter's book is by Oxford Science Publications, 1990.  It's good.
(Great historical bits.)  All 10 zillion equivalents of AC in various
branches of mathematics are mentioned.

        re .0,
        
>(AC) A direct product of non-empty sets is non-empty.
>
>(WAC) Consider a non-empty set. Then we can choose an element of this set.
        
        The second "falls out" of the first order logic in which set
        theory is usually embedded.  There are many "equivalent"
        formulations of first order logic.  One may have a symbol
        upside-down E for "there exists" and another may have only the
        upside-down A for "for all" and use (Ex)(F(x)) as an
        abbreviation for ~((Ax)(~F(x))).  One may have the "constant
        introduction rule" that if in a proof you have derived
        (Ex)(F(x)), then you can introduce a constant symbol b not yet
        used in the proof and add F(b) to your proof.  In other
        formulations this rule is just a convenience, and "unofficial
        proofs" which use it and be mechanically transformed into
        "official proofs" which don't.  In either case, if a is shown
        to be a non-empty set then you can show (Ex)(x \in a) where \in
        represents the Greek letter epsilong used to denote "is an
        element of".  Then "constant introduction" lets you formally
        or informally invent a new constant symbol b such that b \in a
        and you can use b in your proof.  If your end result doesn't
        mention b, then even in the informal case, you can still
        transform the unofficial proof using b to an official proof of
        your end result.
        
        Dan