According to Wikipedia:

Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin. In many cases such a selection can be made without invoking the axiom of choice; this is in particular the case if the number of bins is finite...

How do we know that we can make a selection when the number of bins is finite? How do we even know that we can make a selection from a single bin of finite elements?

Then it gives an example:

To give an informal example, for any (even infinite) collection of pairs of shoes, one can pick out the left shoe from each pair to obtain an appropriate selection, but for an infinite collection of pairs of socks (assumed to have no distinguishing features), such a selection can be obtained only by invoking the axiom of choice.

But how can we even make a selection out of a single pair of socks if they don't have any distinguishing features? Is there another axiom being assumed here?

  • $\begingroup$ I guess there are a few related post on the site. For example: Axiom of Choice and finite sets $\endgroup$ – Martin Sleziak Mar 2 '17 at 4:58
  • $\begingroup$ Somewhat of a "reverse question", math.stackexchange.com/questions/1318441/…, you might want to look at the comments on my answer there as well. $\endgroup$ – Asaf Karagila Mar 2 '17 at 9:46
  • $\begingroup$ I think it's worth noting that in a constructive setting, the axiom of choice, suitably formulated, implies the law of excluded middle and that this proof only involves using the axiom of choice on "finite" sets. (Though, the notion of "finite" splits into multiple different concepts constructively.) The point being that the axiom of choice is saying something non-trivial even for finite sets. $\endgroup$ – Derek Elkins left SE Mar 2 '17 at 21:30
  • $\begingroup$ @Derek: And in other situations the axiom of choice is in fact a theorem. Especially if you have a family of inhabited sets, then you should have an algorithm proving that each of the sets has an element, and that gives you a choice function. Namely, if you constructed the family of the sets, and they were all constructed and non-empty, then you should be able to construct a choice function. Of course, "not empty" and "inhabited" are different things in constructive settings. (And take all that I said above with a grain of salt, as it applies to some, but not all, constructive settings.) $\endgroup$ – Asaf Karagila Mar 3 '17 at 15:39
  • $\begingroup$ @AsafKaragila: I'm interested in learning more about the "meta-finite integers", but a Google search seems to indicate these comments as the only reference. Do they go by another name? $\endgroup$ – RghtHndSd Aug 19 '19 at 21:36

It's a matter of the basic rules of inference allowed in proofs.

Suppose $\mathcal B$ is a "collection" of bins with only one element, i.e., $\mathcal B = \{S\}$ for some set $S$. The assumption is that $S$ is nonempty. By definition, this means there exists $x \in S$. We can use the existential instantitation rule of inference to fix $x \in S$. Then the association $$\mathcal B \to \bigcup_{T \in \mathcal B} T = S$$ given by $$\{S \mapsto x\}$$ defines a choice function.

Similarly, one can prove by induction that if $\mathcal B$ is a finite collection of nonempty buckets, then a choice function exists - if $\mathcal B_n$ is a collection of $n$ nonempty buckets, then fixing $S \in \mathcal B_n$, it follows that $\mathcal B_n \setminus \{S\}$ is a collection of $n-1$ nonempty buckets.

  • $\begingroup$ If $n$ is $1$, $\mathcal B_n \setminus \{S\}$ is $\mathcal \varnothing$, correct? Is it fair to call it a collection of zero nonempty buckets? (Serious if tangential question.) $\endgroup$ – David Moles Mar 2 '17 at 17:50
  • 4
    $\begingroup$ @David: All the members of the empty set are non-empty sets themselves. Disagree? Show me a counterexample! :) $\endgroup$ – Asaf Karagila Mar 2 '17 at 19:13
  • 1
    $\begingroup$ @Dustan: One has to be careful about "by induction". External induction can only take you through the meta-finite integers; internal induction can get you through all the integers of the universe. Of course, this is a delicate point and we can ignore it for the sake of beginnings; but it should always be remarked that this is somewhat delicate. $\endgroup$ – Asaf Karagila Mar 2 '17 at 19:14
  • $\begingroup$ @AsafKaragila I figured the induction part would probably be more complicated. I think that's your turf more than mine. :) $\endgroup$ – Dustan Levenstein Mar 2 '17 at 21:23
  • $\begingroup$ Actually, your proof works just fine. It's just something that one needs to pay attention to: you can treat your proof as iterated existential instantiation, which would only work for meta-finite integers; or as using the fact ZF proves induction, and that if two families admit a choice function, then their union admits a choice function (in the process here we use existential instantiation, but differently). $\endgroup$ – Asaf Karagila Mar 3 '17 at 14:12

The axiom of choice says precisely that if $I$ is a set and, for each $i \in I$, we have a non-empty set $X_i$, then the product $\prod_{i \in I} X_i$ is non-empty. (Elements of products can be identified with choice functions, so non-emptiness of the product is equivalent to existence of a choice function.) When $I$ is finite, this is a statement which can be proved by induction on $|I|$, which does not require choice.

  • $\begingroup$ It seems for me that this is a bit more complicated. For a finite set of indexes products can be simply defined as ordered tuples (which can be defined inductively from an ordered pair). And induction argument works for that definition. On the other hand products can be defined as sets of choice functions (this definition is particularly useful for infinite sets of indexes). Now for your argument to work you would have to prove that these two definition are "equivalent" in the finite case, right? $\endgroup$ – freakish Mar 2 '17 at 0:20
  • 1
    $\begingroup$ Don't we need to say "if $I$ is a non-empty set, and..."? $\endgroup$ – Chas Brown Mar 2 '17 at 8:40
  • 1
    $\begingroup$ @ChasBrown: no, it’s fine as stands! If $I$ is empty then the product $\prod_{i \in I} X_i$ has a unique element, so is non-empty as claimed. $\endgroup$ – Peter LeFanu Lumsdaine Mar 2 '17 at 10:32
  • 3
    $\begingroup$ The problem I have with this answer is that it doesn't address the fact that, in the induction step, we have to choose an element of this new added set (so we essentially reduce to one-set AC). The reason I think it might be confusing is that some common expositions involving AC may imply that we need to construct an element of the set (which we don't). $\endgroup$ – Wojowu Mar 2 '17 at 16:46
  • 1
    $\begingroup$ @Neel: The empty function is indeed a choice function from the empty family. $\endgroup$ – Asaf Karagila Mar 3 '17 at 15:35

This is a good question; the main answer is that making a single choice out of a single bin is a matter of logic.

Specialized to this particular situation, if $S$ is a set and you have proven $\exists x : x \in S$, then logic allows you to introduce a new constant symbol (say, $a$) along with the corresponding an axiom $a \in S$.

The usual interpretation of this mechanic is that $a$ represents a 'choice' of an element of $S$, although this is by no means the only way to interpret this sort of thing:

  • We might instead interpret $a$ as simply being a dummy variable, so that what we're doing is defining a function of $S$
  • We might interpret $a$ as some sort of 'generic' element of $S$ rather than a choice of a specific element
  • Some forms of logic allow you to introduce $a \in S$ even when $S$ is an empty set; naturally this does not lend itself well to interpreting $a$ as a choice of an element!

Whatever way we look at it, we can use it to prove we can make a choice from a single bin in set theory; the main steps are

  • Introduce $a \in S$
  • Show $\{ (S, a) \}$ is a choice function on $\{ S \}$

Whatever our philosophical opinions on logic are, this construction defines a function

$$ S \to \operatorname{ChoiceFunctions}(\{ S \}) $$

where $\operatorname{ChoiceFunctions}(X)$ means the collection of all choice functions on $X$. This, together with the hypothesis that $S$ is nonempty, implies that $\operatorname{ChoiceFunctions}(\{ S \}) $ is nonempty as well.

Finite choice is basically the same. In an ad-hoc fashion you could repeat this sort of argument by repeatedly introducing one variable at a time. Alternatively (in set theory) you can set up a recursive definition and show finite choices can be made by induction; IIRC the proof is straightforward, but complicated.


This isn't a direct answer to the question, but a way to think about the axiom of choice.

The axiom of choice is a generalization of finiteness. It's related (by, for instance, the compactness theorem in logic, and Tychonoff's theorem in topology) to topological compactness, which is another generalization of finiteness.

Without the axiom of choice, you can sometimes specify a choice: "Pick the left shoe from each pair." If you can make (read: define) such a specification, you don't need the axiom of choice, because you can point to that specification as your choice.

Consider how each equivalent definition of Choice is true in the finite setting:

  • "Every finite product of non-empty sets has at least one element." If you're given a few sets, you can select one from each, one step at a time. (If you have an infinite number of sets, you'd need an infinite number of steps.)
  • "Every finite set can be well-ordered." If you pull elements out one at a time, that's a well-ordering. (Again, you'd need an infinite number of steps for an infinite set.)
  • "Every finite vector space has a basis." Choose a non-zero vector. Then take a vector not in the linear subspace generated by the first vector. Then take a vector not in the span of the first two vectors. Eventually, you'll run out of vectors.
  • "Every two finite cardinals are comparable." Count up from 0 until you get to the first one. That's the smaller one. If you get to both at once, they're equal.

In an informal sense, the axiom of choice says you can always take an infinite number of (certain kinds of) steps in finite time. And you can only follow a statement/proof that takes finite time to read. The axiom of choice is also non-constructive: you can't use it to make a "real" example, because you'd need infinite construction time.

More on finiteness and statements:

Let $X = X_0 \times X_1 \times X_2 \times \dots$ be a product of sets. Then the axiom of choice says

$$\exists x_0 \in X_0 \ \exists x_1 \in X_1 \ \exists x_2 \in X_2 \ \exists \dots \ \text{s.t.} (x_0, x_1,x_2, \dots) \in X$$

But the first ellipsis doesn't actually make sense in logic. No mathematical logic rules allow an infinite number of quantifiers. The axiom of choice sort of says, "That's okay, it still works."

On the other hand, you can define the "left shoe" choice with only a finite number of quantifiers. Let $I$ be the index set for the product. Then

$$\{\text{left}_i \in X_i | i \in I\} \in X$$

is a choice of all the left shoes, with one implicit quantifier over the index set.

  • $\begingroup$ See the comment I left to Dustan on the accepted answer, it is relevant here. This method only lets you get through the meta-finite integers, not through all the integers of the universe. And while this might be "sufficient" for most mathematicians and it is certainly a good way to present this naively, this method still misses a large chunk of relevant information about the interactions of theory and meta-theory when it comes to foundations of mathematics. $\endgroup$ – Asaf Karagila Mar 2 '17 at 19:16
  • $\begingroup$ @Asaf I'm not sure I understand what you're talking about. I think you're talking about nonstandard natural numbers, and how they can't be reached using "steps". I did mean to add some comments about this relying on induction (I had ultrafinite mathematics in mind), and another about ordinals and transfinite induction. I couldn't solidify the thoughts, though. I'm admittedly rusty, and intended this to be an informal answer. Everyone should feel free to add any necessary caveats to my answer. $\endgroup$ – leewz Mar 2 '17 at 23:37
  • $\begingroup$ The second part of your answer is based on the misconception that iterating the binary cartesian product is just the same as forming the collection of sequences such that the $k$-th item in each sequence is from the $k$-th set. For finitely many sets it is non-trivial and has to be done carefully to avoid merely getting cartesian products of meta-finite length (as per Asaf's comment), and a proof that they are the same is still lacking. For infinitely many sets it is simply meaningless. And the axiom of choice does not actually state anything about cartesian products... $\endgroup$ – user21820 Mar 3 '17 at 6:50

If I buy a pair of white socks, and I have never worn either of them, then they don't have any distinguishing features. Nevertheless, people make these sort of choices on a daily basis.

You might argue, while indiscernible, the two socks surely have some feature which distinguishes them! And you'd be correct. Although you might not be able to actually point the finger and say "Aha! This is what distinguishes them!", and you might have to resort to something like their particles or some other microscopic-level sort of difference.

But if I now ask you to choose from several pairs at the same time, you first need to inspect each pair under a microscope (or some other more destructive tests) in order to be able to describe a choice process. Maybe in one pair the cotton impurity is higher in one, and maybe in another it is the same. So each pair needs to go under careful checks just so you can tell me what sock was chosen from each pair.

Of course, you can ditch this method, and just go "This sock, that sock, this sock, and that sock". But that is not going to work if you have infinitely many socks.

And indeed, in the formal version of the socks analogy—which is all that it is, an analogy, and we would do well to remember that—we have sets of two elements and we cannot choose from all these pairs simultaneously. Of course, given one pair, we can show there are differences between the two elements of the set, after all they are not the same element, but we cannot point at a single property that will work for all pairs at the same time. Which is why the axiom of choice is needed in such case.


This is essentially just the power of the pairing axiom. Consider the case $n=3$: If $A,B,C$ are nonempty, then so is $A\times B\times C$. The proof of this is easy: if $x\in A,y\in B,z\in C$, then $(x,y,z)\in A\times B\times C$.

We can write this schematically as:

$$\exists x\exists y\exists z\,((x,y,z)\in A\times B\times C)\implies \exists w\,(w\in A\times B\times C),$$

where we can see the pairing axiom (which asserts that $(x,y,z)$ is a set) doing the work of compressing $n$ existence quantifiers into one.

I want to make it clear that there is no actual choosing going on here. It is not required that there be any rule to find a particular element of $A$ - they might be "indistinguishable socks" for all we care. It doesn't matter, because the ambiguity of the original choices has been off-loaded to ambiguity in the output element of $A\times B\times C$.

The problem with this method is that pairing only works for $n=2$, or by induction, for finite $n$. Beyond this we must postulate an axiom or use additional structure in the $A_i$ sets in order to produce choice functions.

  • $\begingroup$ I upvoted this answer because I think it explains it the most clearly. That doesn't mean the other answers aren't good because it's easy for experts to show that adding the rule of inference of existential instantiation to ZF still ends up giving a formal system equivalent to ZF. $\endgroup$ – Timothy Aug 7 '18 at 0:47
  • $\begingroup$ I find ZF a bit dubious. I don't really feel super sure that for any pair of nonempty sets at all, there exists an ordered pair of an element of the first set and an element of the second set. However, once you decide that the real meaning of that statement is a certain statement that's describable in the formal system of ZF, then it's easy to show that the formal system of ZF is consistent and proves that statement. I think this answer is a good answer because it's enough for its formal meaning to be provable in the formal system of ZF and it doesn't need to actually be true. $\endgroup$ – Timothy Aug 7 '18 at 16:45
  • $\begingroup$ @Timothy The only thing ZF is bringing to the table is that for any two sets $a,b$ there exists a set that is the pair $(a,b)$. All the rest is pure first order logic. Let me put it a bit more logically. We want to prove $\exists a,a\in A,\ \exists b,b\in B\vdash\exists w, w\in A\times B$, and FOL says it suffices to prove $a\in A,\ b\in B\vdash\exists w,w\in A\times B$. Now the pairing axiom says that we can take $w=(a,b)$ because this is a set, and then the statement is true by definition. $\endgroup$ – Mario Carneiro Aug 8 '18 at 1:12
  • $\begingroup$ I already saw how it was possible to prove it in ZF. I don't know how to write a formal proof in ZF but I seem to have good intuition of what's provable in it. If I learned how to write a formal proof in it, I'd probably be able to figure out how to write a formal proof of the statement that for any finite set of nonempty sets, there is a choice function, but that doesn't mean I will be willing to claim to have figured out a proof that ZF is a true model of set theory. $\endgroup$ – Timothy Aug 8 '18 at 1:17
  • $\begingroup$ @Timothy My point is that you should actually look into formal proofs in first order logic first. In particular, see if you can understand the $\exists L$ rule in en.wikipedia.org/wiki/Sequent_calculus#Inference_rules , I think this will help. Because I would bet that your intuitions don't have any trouble with the claim that $a\in A,\ b\in B⊢∃w,w∈A×B$, because in this case the "choice" has already been made: you are given $a\in A$ and $b\in B$ and wish to prove the product is nonempty. The only thing between this and the full proof is that $\exists L$ rule of FOL. $\endgroup$ – Mario Carneiro Aug 8 '18 at 3:17

But how can we even make a selection out of a single pair of socks if they don't have any distinguishing features? Is there another axiom being assumed here?

I wish to address a misconception here. The axiom of choice does not concern picking an object from indistinguishable ones, but rather that we do not need a way to distinguish them to be able to pick one of a collection. For example consider any infinite group $G$. There is no way you are going to be able to uniquely identify a non-identity element in $G$, because you know nothing about $G$. But the axiom of choice (applied to the non-identity elements in $G$) states that we can indeed pick one of them. Of course, since we only have one picking to do, we do not need the axiom of choice at all. But this illustration is to make clear what exactly is the issue of picking; the objects in each non-empty set may very well be distinguishable but we do not care.


This is a rider to the excellent answers given by Clive and Dustan. To address the case of a single pair of socks: assume you are given an unordered pair of socks $\{x, y\}$ such that the socks $x$ and $y$ have no distinguishing features. Then $x$ and $y$ are the same sock. In this case, you should take the sock back to the store and claim Leibniz's law of the identify of indiscernibles as an unchallengeable reason for a refund.

  • 1
    $\begingroup$ @RobinSaunders: we are taking about set theory here. If you have constructed a set theoretic model of the complex numbers it will contain two distinct square roots of $-1$. Set theory doesn't give you the option to abstract away representational differences. I would agree that this is from many points of view a weakness in set theory. $\endgroup$ – Rob Arthan Mar 2 '17 at 20:48
  • 2
    $\begingroup$ @RobinSaunders: $i$ and $-i$ are only indistinguishable from the point of view of the first-order theory of fields. But to get the complex numbers we must have proven the existence of a model of the field axioms that contains the reals and has a square-root of $-1$. In any such model the two square-roots of $-1$ will be different. Labels are irrelevant. Just because conjugation is an isomorphism does not make $i$ and $-i$ in any such model indistinguishable, exactly like negation is an isomorphism on $(\mathbb{Z},<)$ but does not make $1$ and $-1$ indistinguishable. $\endgroup$ – user21820 Mar 3 '17 at 6:15
  • 2
    $\begingroup$ @RobinSaunders: Also, as Rob says, there are certain practical issues in using pure set theory, since the axiom of extensionality implies that structures with different underlying sets are distinct even if there is an isomorphism between them. This is not a serious technical issue, since we can endeavour to prove theorems about the abstraction rather than a concrete representation. For example it is better to prove theorems about arbitrary structures isomorphic to $\mathbb{N}$ (or if possible just models of PA) rather than a specific representation of the natural numbers. $\endgroup$ – user21820 Mar 3 '17 at 6:31
  • 2
    $\begingroup$ @RobinSaunders: that's what model theory using set-theoretic foundations is like. "Indistinguishable" in set theory has to mean "indistinguishable as sets" and if a model needs to contain $2$ objects with some property, then they will be distinguishable as sets, even if the abstract structure we are trying to model gives us no way to distinguish them. $\endgroup$ – Rob Arthan Mar 5 '17 at 22:44
  • 1
    $\begingroup$ @RobinSaunders: Once again, as Rob says, you need to distinguish (pun not intended) between what the axiomatization can 'see' and what the meta-system can see. Worse still, the entire theory of the structure may be unable to distinguish between certain elements using a formula over the language, and these elements are called "indiscernibles" (see David Marker's introduction to model theory). For a simple example, in the graph that looks like o-o-o, there is no formula over the language of adjacency that distinguishes the 2 end nodes, but the meta-system considers them 2 distinct objects. $\endgroup$ – user21820 Mar 6 '17 at 6:57

Suppose discourse universe is formed by objects. Starting with

Axiom 1 (Empty set). There exists a set $\emptyset$ such which contains no elements, i.e., for every object we have $x\notin\emptyset$.

We can prove by contradiction the folling proposition:

Proposition 2 (Single choice). Let $X$ be a non-empty set. Then there exists an objects $x$ such that $x\in X$.

Now we can show that for any collection of non-empty sets, we can choose a element for each set. (Use induction to prove it.)

Proposition 3 (Finite choice). Let $n\ge1$ be a natural number, and for each natural number $1\le i\le n$, let $X_i$ be a non-empty set. Then there exists an $n$-tuple $(x_i)_{1\le i\le n}$ such that $x_i\in X_i$ for all $1\le i\le n$. In other words, if each $X_i$ is non-empty, then the set $\prod_{1\le i\le n}X_i$ is also non-empty.

The axiom of choice asserts that this proposition is also true for infinite cartesian products.

Axiom 4 (Choice). Let $I$ be a set, and for each $\alpha\in I$, let $X_\alpha$ be a non-empty set. Then $\prod_{\alpha\in I}X_\alpha$ is also non-empty. In other words, there exists a function $(x_\alpha)_{\alpha\in I}$ which assigns to each $\alpha\in I$ an element $x_\alpha\in X_\alpha$.

This is very intuitively appealing axiom; in some sense one one is just apllying Proposition 2 over and over again. But it does not follow from the other axioms of set theory.


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.