$\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.)

  • 2
    $\begingroup$ Many people are not explicit about where they invoke AC. I don't understand your notation. What does Set.I mean? $\endgroup$ – Qiaochu Yuan Mar 29 '11 at 18:36
  • 2
    $\begingroup$ 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. $\endgroup$ – Arturo Magidin Mar 29 '11 at 18:42
  • $\begingroup$ @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. $\endgroup$ – joriki Mar 29 '11 at 18:51
  • $\begingroup$ @Qiaochu Yuan ♦: The dot in “Set.I” is a part of syntax of $\forall$. $\endgroup$ – beroal Mar 30 '11 at 9:16
  • 3
    $\begingroup$ @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. $\endgroup$ – 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.

  • $\begingroup$ We answered this at the same time, it seems. I think your proof emphasizes the duality better than mine. $\endgroup$ – Carl Mummert Mar 29 '11 at 19:12
  • $\begingroup$ 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? $\endgroup$ – Carl Mummert Mar 29 '11 at 19:26
  • $\begingroup$ @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. $\endgroup$ – Apostolos Mar 29 '11 at 19:48
  • $\begingroup$ @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$. $\endgroup$ – Arturo Magidin Mar 29 '11 at 19:50
  • $\begingroup$ @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$. $\endgroup$ – 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.

  • $\begingroup$ 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$. $\endgroup$ – Arturo Magidin Mar 29 '11 at 19:15
  • $\begingroup$ Sure, but the axiom of regularity is part of ZF. $\endgroup$ – Carl Mummert Mar 29 '11 at 19:17
  • $\begingroup$ Oh, absolutely; did not mean to imply otherwise... $\endgroup$ – Arturo Magidin Mar 29 '11 at 19:17
  • $\begingroup$ 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$... $\endgroup$ – Carl Mummert Mar 29 '11 at 19:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.