picking a witness requires the Axiom of Choice?

$\forall I, A:Set. I\subseteq \bigcup A\to \exists f:I\to A. \forall i\in I. i\in f(i)$

Does this theorem require the Axiom of Choice? To prove, I need to find $\forall i\in I$ a witness of that $i\in \bigcup A$. Any witness $B$ is such that $i\in B\land B\in A$. There may be more than one witness, but I must return one, a choice function will pick it. I define a function $w_S:I\to P(A), w_S(i) := \{B\in A|i\in B\}$, $w_S$ returns a set of witnesses. $im(w_S)$ satisfies the hypothesis of the Axiom of Choice, then I construct a choice function $c:im(w_S)\to A$ and return $c\circ w_S$.

The “relation→function” form of the Axiom of Choice from Equivalent statements of the Axiom of Choice is also suitable for the proof.

AFAIK if the Axiom of Choice is used in a proof, then the proof explicitly says that. But I came across some proof similar to my theorem which does not mention the Axiom of Choice, so I am unsure.

(Update 2011-03-30. My theorem above is required for this theorem: $\forall A,B:Set. finite(A) \land A\subseteq \bigcup B \to \exists B'\subseteq B. finite(B')\land A\subseteq\bigcup B'$ which intuitively is “every finite set is compact”. It is implicitly used here, theorem 3.2.2.)

(Update 2011-03-31. It turned out that my theorem is not required for the theorem in “Update 2011-03-30”. That is a good example to learn in what cases the Axiom of Choice is required.

I rewrote Apostolos's proof:

Proof. Assume that $X$ is a set of inhabited sets. Define $i(b) := \{B\in X | b\in B\}\cup\{\{b\}\}, dom(i)=\bigcup X$. Assume that $i(b_0)=i(b_1)$, then $\{b_0\}\in i(b_1)$, then $(\{b_0\}\in X \land b_1\in\{b_0\}) \lor b_0=b_1$, left disjunct also implies $b_0=b_1$. Then $i$ is an injection. Then $i:\bigcup X\to im(i)$ is a bijection. Assume that $B\in X$, then $B$ is inhabited, take $b, b\in B$, by definition of $i$ $B\in i(b)$, obviously $i(b)\in im(i)$. Then $X\subseteq (im(i))$. By my theorem, take $w:X\to im(i)$. By $i$ being a bijection, define $c:X\to\bigcup X, c := i^{-1}\circ w$. Assume that $B\in X$, then $w(B) = i(c(B))$, then by definition of $w$ $B\in w(B)$, then by definition of $i$ and $c$ $c(B)\in B$. Then $c$ is a choice function. Qed.)

• Many people are not explicit about where they invoke AC. I don't understand your notation. What does Set.I mean? – Qiaochu Yuan Mar 29 '11 at 18:36
• It is false that "if the Axiom of Choice is used in a proof, then the proof explicitly says that." Many times people don't mention it, or mention statements that are equivalent but not widely known to be (e.g., "take a basis for the vector space"; turns out "every vector space has a basis" is equivalent to the Axiom of Choice). Simply put, just because a proof does not say so explicitly does not, in and of itself, imply that AC is not used. – Arturo Magidin Mar 29 '11 at 18:42
• @Qiaochu: I think periods are being used as delimiters here, and "$I, A: Set$" looks like a type declaration, i.e. $I$ and $A$ are sets. @beroal: I believe this does require choice. If you tell us about the other proof that didn't mention choice, we might be able to tell whether and where it's "hidden" there. – joriki Mar 29 '11 at 18:51
• @Qiaochu Yuan ♦: The dot in “Set.I” is a part of syntax of $\forall$. – beroal Mar 30 '11 at 9:16
• @beroal: You don't need choice (and hence don't need your theorem) for the theorem in your update. Because $A$ is finite, you only need a finite number of choices to construct $B'$ in the same way that you do it for arbitrary sets in your theorem. – joriki Mar 30 '11 at 10:02

This is equivalent to the axiom of choice. Take a set $X$ of non-empty sets. Let the set $X'= X\cup\{\{x\} : x\in\bigcup X\}$ and for every $x\in\bigcup X$ take $C_x=\{y\in X' : x\in y\}$. Observe that if $x\neq y$ then $C_x\neq C_y$ since $\{x\}\in C_x$ while $\{x\}\notin C_y$. The set $A=\{C_x : x\in\bigcup X\}$ is a set through the axiom of replacement and you have that $\bigcup A=X'$. If there is a function $f:X'\to A$ satisfying the statement you wrote you have a choice function $g$ for $X$, namely $g(y)=x\iff f(y)=C_x$.

The fact that the axiom of choice is enough to show the statement you wrote is easy.

• We answered this at the same time, it seems. I think your proof emphasizes the duality better than mine. – Carl Mummert Mar 29 '11 at 19:12
• Now that I look at it again I have a concern: in general, I don't see how to uniquely recover $x$ just from the set $C_x$; maybe there are $x, x'$ with $C_x = C_{x'}$. Is there some way to work around that? – Carl Mummert Mar 29 '11 at 19:26
• @Carl: Thank you for noticing it. I'll take a look at it and if I can't find a means to circumvent the axiom of choice I will remove my answer. – Apostolos Mar 29 '11 at 19:48
• @Carl: You could use the equivalent version of Choice that begins with a set of nonempty, pairwise disjoint sets; or replace $X$ with $X' = \{x\times\{x\}\mid x\in X\}$ before proceeding, so that $C_x = C_y\Longleftrightarrow x=y$. – Arturo Magidin Mar 29 '11 at 19:50
• @Arturo Magidin: The first of those won't help; if the sets in $X$ are pairwise disjoint you will certainly get $C_x = C_{x'} = \{y\}$ whenever $x,x' \in y \in X$. This is the extreme case for failure to recover $x$ from $C_x$. – Carl Mummert Mar 29 '11 at 19:54

Yes, this requires the axiom of choice. Suppose that $\mathcal{C}$ is any family of nonempty sets. Take the family $$\mathcal{D} = \{ \{X, \langle X, a\rangle\} : X \in \mathcal{C}, a \in X \}$$ where $\langle \cdot,\cdot\rangle$ denotes an ordered pair. Note that $\langle X,a\rangle \not = X$ for all sets $X,a$ if we use the usual definition of an ordered pair in set theory.

Now $\mathcal{C} \subseteq \bigcup \mathcal{D}$, because each set in $\mathcal{C}$ is nonempty. Assuming your principle holds, let $f \colon \mathcal{C} \to \mathcal{D}$ be such that $X \in f(X)$ for each $X \in \mathcal{C}$. Then we can define a choice function $g$ on $\mathcal{C}$ with the rule: $g(X)$ is the unique set $a$ such that $\langle X,a\rangle \in f(X)$. This definition does not require the axiom of choice because $g(X)$ can be defined explicitly.

• Don't you need the Axiom of Foundation/Regularity, and not just the usual definition of ordered pair, to conclude that $\langle X,a\rangle\neq X$? Say $a=\{a\}$. Then $\langle \{a\},a\rangle = \{\{\{a\}\},\{\{a\},a\}\} = \{\{a\},\{a\}\} = \{\{a\}\} = \{a\} = a$. – Arturo Magidin Mar 29 '11 at 19:15
• Sure, but the axiom of regularity is part of ZF. – Carl Mummert Mar 29 '11 at 19:17
• Oh, absolutely; did not mean to imply otherwise... – Arturo Magidin Mar 29 '11 at 19:17
• Actually, even if $X = \langle X,a\rangle$ for some $a \in X$ my construction would work, as long as this only happens for at most one value of $a$... – Carl Mummert Mar 29 '11 at 19:17