Why can't Axiom of Choice be proven by Rule C Rule C is appeared in the textbook: Introduction to mathematical logic by Mendelson (Page 81 in the fourth edition). It is said "It is very common in mathematics to reason in the following way. Assume that we have proved a wf of the form $(\exists x)(B(x))$. Then we say, let $b$ be an object such that B(b). We continue the proof, finally arriving at a formula that does not invovle the arbitrarily chosen element $b$..........In fact, we can achieve the same result without making an arbitrary choice of element $b$". So if you have a proof using Rule C, you can also have another proof without using Rule C.
Now return to the Axiom of Choice. The axiom says that "Let $I$ be a set, and for each $\alpha \in I$, let $X_{\alpha}$ be a non-empty set. Then $\Pi_{\alpha \in I} X_{\alpha}$ is also non-empty." In other words, there exists a function $f:I \rightarrow \cup_{\alpha \in I}X_{\alpha}$ which assigns to each $\alpha$ an element $x_{\alpha} \in X_{\alpha}$. It seems that there is an obvious proof for it by Rule C: Since $\forall \alpha$, $X_{\alpha}$ is non-empty, there exists some element in $X_{\alpha}$. let $b$ be the element. So we assign $\alpha$ the element $b$. So $\forall \alpha$, we can assign an element. So the function exists.
Clearly the above proof uses Rule C. The proof can be transformed to another proof without Rule C. So there is a proof for the Axiom of Choice.
Since the Axiom of Choice has been proven to be independent, the above proof is wrong. But I failed to find it. Anybody can help me?
 A: Suppose that a family $X$ has only two elements, $X_1$ and $X_2$. Then, if $X_1$ is nonempty we can use Rule C to obtain some $b_1 \in X_1$. Also, if $X_2$ is nonempty, we can use Rule C to obtain some $b_2 \in X_2$. Then we can explicitly define a choice function $f$ on $X$ by the rule 
$$
f(x) = y \Leftrightarrow ( x = 1 \land y = b_1) \lor (x = 2 \land y = b_2).
$$
Note that $b_1$ and $b_2$ are new symbols in our formal language that were introduced by Rule C. 
We can do the same thing for any finite family of nonempty sets, by induction. We can always add one more point to the domain of an existing choice function, using Rule C to "choose" the value of the function at that point. 
But what if $X$ is an infinite family of nonempty sets? We can still find an element of $X_i$ for each member $X_i$ of $X$. But we will no longer be able to write down a single, finite formula that defines the choice function.  Any finite formula could only have finitely many new variables that were introduced by Rule C, but the naive approach to proving the axiom of choice from Rule C would require one such variable for every element of the set. (It is not even clear there is a term for each element of the index set $I$.)
That is why Rule C does not allow us to prove the axiom of choice, in general. To form the choice function, we would need to define the choice function by a finite formula and then apply a set existence axiom, but in the cases where the axiom of choice is needed there is no explicit definition of a choice function. 
This shows that the axiom of choice might be better named the "axiom of making infinitely many choices simultaneously".
A: The problem with the axiom of choice is that there is no method that can select an element from EVERY set. 
So, given a set $M$ , we cannot guarantee that the axioms of $ZFC$ allow a selection of an element of $M$, although there must be some, if $M$ is non-empty.
A: Your confusion here reminds me of the old saying "The axiom of choice is clearly true, the well-ordering principle is clearly false, and who can say about Zorn's lemma?"
While for any $\alpha$, you can choose an $x_\alpha \in X_\alpha$, you need the axiom of choice to show that this can be stitched together into a full choice function that is simultaneously valid for all $\alpha$. In other words, the axiom of choice takes you from the statement $\forall \alpha(\exists x_\alpha \in X\alpha)$ to the statement $\exists f(\forall\alpha(f(\alpha) \in X_\alpha))$
