27
$\begingroup$

The axiom of choice asserts the existence of a choice function for any family of sets F. Suppose, however, that F is finite, or even that F just has one set. Then how do we prove the existence of a choice function?

The usual answer is that we just go from set to set, picking an element from each set. Since F is finite, this process will terminate. What I'm really wondering is how we can always choose from a single set. The informal answer seems to be just that it's possible... but this isn't an axiom, so it must be justified some other way.

So: how do you prove from the axioms of just ZF without choice, that for any nonempty x there exists a function f:{x}->x?

Improve this question
$\endgroup$
6
  • 5
    $\begingroup$ By definition of "nonempty", x contains an element y, so let $f$ be given by the set of ordered pairs {({x}, y)}. $\endgroup$
    – Charles Staats
    Commented Jul 19, 2010 at 21:29
  • $\begingroup$ Sorry, that should be {(x, y)}. $\endgroup$
    – Charles Staats
    Commented Jul 19, 2010 at 21:33
  • $\begingroup$ Well, saying the product is non-empty is equivalent to the axiom of choice. I assume the OP means, how do we show this claim from the axioms? $\endgroup$
    – Daniel Litt
    Commented Jul 19, 2010 at 21:37
  • $\begingroup$ The product is, by definition, the set of all ordered pairs. In this case, we can explicitly write down an ordered pair, so clearly the product is nonempty. But I'm not entirely sure I understand your comment, so my apologies if this comment does not address it. $\endgroup$
    – Charles Staats
    Commented Jul 19, 2010 at 21:41
  • $\begingroup$ Ah sorry; I think the OP's question boils down to: how, from the axioms of ZF, do we "explicitly write down an ordered pair"? Since if we can write down ordered pairs, we're obviously done. $\endgroup$
    – Daniel Litt
    Commented Jul 19, 2010 at 21:48

4 Answers 4

Reset to default
30
$\begingroup$

Although the answers already given are correct, let me add some information (essentially just rephrasing the bracketed part of Thomas Scanlon's answer) that I've found useful for students who raised this question. Consider the problem, at the end of the original question, of "choosing" from a single set $x$. As several people have pointed out, we are given the existential statement, "There is an element in $x$." What should be noticed in addition is that what we want to prove is also an existential statement, "There is a choice function." We have an explicit construction, which I'll call $C$, that will convert any element of $x$ into a choice function, namely sending any $y$ to $\{(x,y)\}$ (as in Charles Staats's comment on the original question). If we can't explicitly define any particular $y$, then we won't be able to define any particular choice function either, but the problem doesn't require us to explicitly define a choice function; we need only prove that one exists. And that follows, thanks to $C$, from the existence of elements in $x$.

Improve this answer
$\endgroup$
3
  • 3
    $\begingroup$ I was in the process of writing this myself, I'll just add one more thing to clarify: As Andreas said, when dealing with a finite number of sets you can explicitly write the function in the form of a formula. However, in the infinite case you cannot write this sort of formula (it would require infinitely many quantifiers to mention which element is chosen) and therefore you're in need of a stronger tool that would guarantee the existence of such function. $\endgroup$
    – Asaf Karagila ♦
    Commented Jul 19, 2010 at 23:47
  • 1
    $\begingroup$ Thank you, this is very helpful. As I indicated in my comments to Thomas Scanlon's answer, my confusion arose because I was looking for an "explicit choice function". $\endgroup$
    – user7758
    Commented Jul 20, 2010 at 0:03
  • 3
    $\begingroup$ @Asaf Karagila: You can only write that formula in the case when the product is externally finite. As the other answers indicate, it is enough that the product is internally finite, in which case an induction argument shows the choice function exists. Moreover, the standard reading of "a finite number of sets" is the internal one. Andreas Blass's comment is safe because he only refers to choosing from a single set. $\endgroup$
    – Carl Mummert
    Commented Jul 20, 2010 at 0:04
29
$\begingroup$

To say that $x \neq \varnothing$ is exactly to assert $(\exists y) y \in x$ and the truth of this existential formula will be witnessed by some set $a$ for which $a \in x$. Thus, the set $f := \lbrace \langle x, a \rangle \rbrace$ is a function from $\lbrace x \rbrace$ to $x$.

[I think that this point, namely that the Axiom of Choice is not used to instantiate the truth of an existential formula by naming a witness is the heart of your question. I am not claiming that there will be a constructive choice of the witness. It is just that if an existential formula is true, there must be a witness.]

More generally, to prove that if $F$ is a finite set of nonempty sets, then $\prod F := \lbrace f : f \text{ a function with dom}(f) = F \text{ such that } (\forall x \in F) f(x) \in x \rbrace$ is non-empty one argues by induction.

If $F = \varnothing$, then the empty function is an element of $\prod F$. If $\text{card}(F) = n+1$, then we may express $F = F' \cup \lbrace x \rbrace$ as disjoint union where $\text{card}(F') = n$. As $x \neq \varnothing$, from the calculation above we find some $f:\lbrace x \rbrace \to x$. By induction, there is some $g \in \prod F'$. I will leave it to you to exhibit a bijection between $\prod F$ and $(\prod F') \times \prod \lbrace x \rbrace$ and thereby complete the argument.

Improve this answer
$\endgroup$
4
  • 9
    $\begingroup$ I think your first point is the main one for the question. It's alluding to the "existential elimination" inference rule, which says that from the assumption $\exists x A(x)$, you can assert $A(c)$ for some new constant $c$. The soundness of the rule is a direct consequence of the way semantics for first-order logic are defined. I have previously encountered confusion from non-logicians about this issue. $\endgroup$
    – Carl Mummert
    Commented Jul 19, 2010 at 22:45
  • 2
    $\begingroup$ @Thomas Scanlon Thanks. Is it true, then, that there isn't a constructive way of choosing the element in general? I think my confusion arose because sometimes people motivate the axiom of choice by saying that for infinite families, there's no "definite procedure" or "explicit method" of choosing your function, so we need to create an axiom. (E.g. en.wikipedia.org/wiki/Axiom_of_choice#Usage) But it seems that even in the finite case, there's no way to explicitly build your function, in one sense of the word "explicit". $\endgroup$
    – user7758
    Commented Jul 20, 2010 at 0:01
  • 5
    $\begingroup$ If you have constructive verification that the set is not empty, you can constructively convert this to a choice function. For example, perhaps you have a constructive proof that the set is nonempty. But if you have no constructive information about the set, of course there's no way to explicitly construct a member of the set, regardless of the axiom of choice. $\endgroup$
    – Carl Mummert
    Commented Jul 20, 2010 at 0:13
  • 1
    $\begingroup$ @Carl: This is true, but it applies to infinite choice just the same (that’s why the axiom of choice is sound under variants of recursive realizability for various constructive theories). $\endgroup$
    – Emil Jeřábek
    Commented Jan 23, 2013 at 11:30
22
$\begingroup$

There are two finite choice theorems, the internal one and the external one, both are true in ZF.

As Charles Staats pointed out, the external version is a tautology (modulo some finite combinatorics): if $a_1,\dots,a_n$ are all nonempty, then there are $z_1 \in a_1$,...,$z_n \in a_n$ and then $\lbrace (a_1,z_1),\ldots,(a_n,z_n)\rbrace$ is the desired choice function for the family $X = \lbrace a_1,\dots,a_n \rbrace$ of nonempty sets.

The internal version "every finite family of nonempty sets has a choice function" is stronger since a model of ZF may have nonstandard finite cardinals. The proof in this case is by induction on the cardinality of the family.

The empty family has a trivial choice function — the empty function. Suppose we know the theorem to be true for families of size $n$. Let $X$ be a family of nonempty sets with size $n+1$. Let $g:n+1\to X$ be a bijection. Let $X' = g[n]$ and $a = g(n)$. Then $X'$ is a family of nonempty sets of size $n$, which therefore has a choice function $f':X' \to \bigcup X'$. Since $a$ is nonempty, we can find $z \in a$ and hence $f = f' \cup \lbrace (a,z) \rbrace$ is a choice function for the original family $X$.

Improve this answer
$\endgroup$
6
  • $\begingroup$ The axiom of pairing is not a tautology... $\endgroup$
    – Emil Jeřábek
    Commented Jan 23, 2013 at 11:26
  • $\begingroup$ Right! That was poorly formulated... $\endgroup$
    – François G. Dorais
    Commented Jan 23, 2013 at 14:01
  • $\begingroup$ Can you please elaborate on your commentary about "nonstandard finite cardinals"? $\endgroup$
    – Matemáticos Chibchas
    Commented Sep 19, 2018 at 19:28
  • $\begingroup$ @MatemáticosChibchas: What is it you want to know? $\endgroup$
    – François G. Dorais
    Commented Sep 19, 2018 at 20:37
  • $\begingroup$ @FrançoisG.Dorais I don't know what a "nonstandard finite cardinal" is (in a model of $\mathsf{ZF}$), sorry. $\endgroup$
    – Matemáticos Chibchas
    Commented Sep 19, 2018 at 21:07
9
$\begingroup$

The Axiom of Choice does not allow to "choose" a choice function, it only says that a choice function exists. To show that a choice function for a single nonempty set exists, you do not need to "choose" an element in the set, it is enough to show that at least one element exists (i.e. the set is nonempty). Every element in the set will give a different choice function.

What did you mean by "choosing" an element from a set? ;)

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .