Choice function

Let $\mathcal{F}$ be a family of sets, every member of which is nonempty. A choice function for $\mathcal{F}$ is a function (A function is a relation $f$ with $(a,b) \in f$ and $(a,c) \in f$ implying $b = c$; $f : A \to B$, the value $f(a)$, domain and codomain) $g : \mathcal{F} \to \bigcup \mathcal{F} \qquad \text{such that} \qquad g(S) \in S \ \text{ for every } S \in \mathcal{F}.$

Given a set $X$, a choice function on $X$ means a choice function for the family $\mathcal{P}(X) \setminus \{\emptyset\}$ (The power set $\mathcal{P}(x) = \{\, z : z \subseteq x \,\}$, The difference $a \setminus b$, the symmetric difference $a \triangle b$, and the complement $X \setminus a$ relative to a set $X$) of nonempty subsets of $X$.

• The requirement is only that $g$ pick some element of each member. Nothing requires the choices to be coherent, definable, or computable, and this is exactly where the difficulty lies: for a single nonempty set $S$ the existence of an element to pick is immediate, and for a family presented as the values of a function on a natural number the picks can be made one after another (Every natural-number-indexed list of nonempty sets has a choice function on its family of values ↗). What is not available in ZF is a simultaneous choice across an arbitrary family.
• A choice function often exists for a concrete family with no appeal to any axiom, because the family carries extra structure that names a canonical element. Every nonempty set of natural numbers has a least element, so $S \mapsto \min S$ is an explicit choice function on $\mathbb{N}$ ($\min$ is a choice function on $\mathbb{N}$ ↗). The contrast with families that admit no such rule is the content of Russell's shoes and socks ↗.
• Members of $\mathcal{F}$ must be nonempty: no function can select an element of $\emptyset$. The family $\mathcal{F}$ itself is allowed to be empty, and the empty function is then a choice function for it.