Defining Choice Functions: When & How Without Using Axiom of Choice

[Hurkyl]

A function f with domain S is a choice function for S if and only if $f(s) \in s$ for all s in S.

 

[Oxymoron]

The Axiom of Choice is equivalent to the statement that every non-empty set has a choice function. [Is this correct?]

If so, then for some sets a choice function can be defined without using the Axiom of Choice. [Is this correct?]

If so, the I may define an explicit choice function for that set.

 

[Hurkyl]

The Axiom of Choice is equivalent to the statement that every non-empty set has a choice function.

No; the AoC is the statement that every set of nonempty sets has a choice function.

Just to make it explicit, the mistakes you made were:
(1) The AoC applies to the empty set. (It's choice function is the empty function)

(2) If S contains the empty set, it cannot possibly have a choice function (you cannot possibly have $f(\emptyset) \in \emptyset$). The AoC applies to all sets that do not contain the empty set.

If so, the I may define an explicit choice function for that set.

If you can explicitly define a choice function, then you can explicitly define a choice function.

An example of an explicitly defined choice function is the following choice function for the set S = {{a}, {b, c}}:

f({a}) := a
f({b, c}) := c

or, as a set-of-ordered-pairs:

f := { ({a}, a), ({b, c}, c) }

 

[CRGreathouse]

If so, the I may define an explicit choice function for that set.

If you have to use AC, then you don't have an explicit choice function, you just know that some choice function exists.