# Does Axiom of Choice naturally hold?

Let $A$ be a set of non-empty sets, then $\bigcup A$ is a set. Furthermore, $(\bigcup A)^{A}$ is a non-empty set. Besides let $P$ be a binary predicate such that for all $X\in A$ there is a unique $x \in X$ satifies $PXx$. $f:=\{(X,x)\in A \times \bigcup A|PXx\}$ is a functional class and $f \in (\bigcup A)^A$. Hence $f$ is also a set.

According things discussed above, $f$ is indeed a choice function of $A$ and is a set. So does this fact means AC is naturally holds?

-
You’ve just demonstrated that if $A$ has a choice function, then $A$ has a choice function. This is true, but hardly earth-shattering. – Brian M. Scott Nov 10 '12 at 7:07
@BrianM.Scott Let me have an explanation. $P$ is not said be a set but a predicate instead. The existence of $f$ only used the Axiom schema of Separation. – Popopo Nov 10 '12 at 7:17
I don't get it. – Asaf Karagila Nov 10 '12 at 7:22
And by assuming the existence of that predicate, you’re assuming the existence of a choice function (via the axiom schema of replacement). – Brian M. Scott Nov 10 '12 at 7:22
@Brian: Good, because I didn't get the geometrical whatchamacallit either. :-) – Asaf Karagila Nov 10 '12 at 7:33

If such $P$ exists then by the replacement schema you have defined a choice function on $A$.
If this $P$ has the property above for all non-empty collections of non-empty sets, then $P$ is actually a function and in fact it is a global choice function.
In either case the predicate $P$ implies that the axiom of choice holds (at least for $A$) and that one can define a canonical choice.
Yes, but what's the difficulty of assuming such a $P$ exists? First let $Pxy$ keeps false for each pair. Since any $X\in A$ is non-empty, $\exists x(x \in X)$ holds for $X$. Thus by logic there is one set $a$ such that $a \in X$ holds, then turn $PXa$ to true and $PXb$ flase for any other $b\ne a$. If the same process terminated for every $X\in A$, then a $P$ was manufactured as required. – Popopo Nov 10 '12 at 8:07
@Popopo: Well, to "exist" is to say that there is a formula $\varphi(X,x,p)$ where $p$ is a parameter such that ZFC proves that $P(X,x)\iff\varphi(X,x,p)$. Using forcing we can add generic sets which will now "confuse" $\varphi$ in the sense that it is not provably whether or not $\varphi$ is true or false for them. In particular this means that we cannot prove global choice from ZF, or even ZFC. If you wish to extend your language and add axioms to describe $P$ as a functional relation between non-empty sets and an element of theirs, then you effectively added global choice. – Asaf Karagila Nov 10 '12 at 8:10
Okay, that means $\varphi(X,x,p)$ is falsifiable in some set models. But I think that only means in some set models some non-empty sets of non-empty sets does not has any choice function as a set. Btw is there any set model in which has at least one non-empty set of non-empty sets which even does not has any choice function which is a class? – Popopo Nov 10 '12 at 8:33
@Popopo: In a model of ZFC we have that $A$ always have a set of choice functions, in fact the only reason we need AC is to prove that this set is non-empty when $A$ is a non-empty collection of non-empty sets. So talking about classes is just when you talk about class-sized collections. E.g. everything. Furthermore any choice function is by definition a set itself, so this is again moot. – Asaf Karagila Nov 10 '12 at 8:43
@Popopo: It is a subset of $A\times\bigcup A$. If it exists then it means that this is a set, because only sets exist. If it was a class it was a class bounded by a set and therefore a set itself. – Asaf Karagila Nov 10 '12 at 9:02