Finite choice without AC

Can anyone explain how we choose one sock from each of finitely many pairs without the axiom of choice? I mean the following quote:
To choose one sock from each of infinitely many pairs of socks requires the Axiom of Choice, but for shoes the Axiom is not needed. The idea is that the two socks in a pair are identical in appearance, and so we must make an arbitrary choice if we wish to choose one of them. For shoes, we can use an explicit algorithm -- e.g., "always choose the left shoe." Why does Russell's statement mention infinitely many pairs? Well, if we only have finitely many pairs of socks, then AC is not needed -- we can choose one member of each pair using the definition of "nonempty," and we can repeat an operation finitely many times using the rules of formal logic (not discussed here).

-
Do you know how to choose one sock from one pair? (Presumably you do this every morning.) –  Qiaochu Yuan Sep 13 '11 at 18:47
In addition to my answer here, you might find some more information in the possibly-too-complicated answer I wrote here. In particular, in the "Added" part toward its end. –  Asaf Karagila Sep 13 '11 at 22:51
@Qiaochu: Why do you ask? Is the answer to the question as simple as what I do every morning? :) –  cabbage Sep 14 '11 at 12:59
As far as I understand I should accept one of the answer, but I don't know how to decide which one is better, I am not yet well acquainted with the topic... –  cabbage Sep 14 '11 at 13:01
@cabbage: yes, more or less. I suppose it depends on how formal you want an answer to be. –  Qiaochu Yuan Sep 14 '11 at 15:28

The main challenge here is explaining the precise set-theoretic statement which is meant by "we can make finitely many choices without the axiom of choice"; the proof is then relatively easy. I am going to write in a sort of semi-formal way, which I hope will be clear enough that you can see how to translate into statements of ZF.

By CHOICE, I mean the statement:

Let $X$ and $Y$ be sets, with a map $\pi: X \to Y$. Suppose that, for every $y \in Y$, there is an $x \in X$ with $\pi(x) = y$. Then there is a subset $K$ of $X$ such that, for every $y \in Y$, there is a unique $x \in K$ with $\pi(x) = y$

So $X$ is the set we are choosing from (the set of all socks in the universe), $Y$ is the number of choices we're making, and $K$ is the set of choices we make.

Now, I want to show that this statement is true if $Y$ is finite. So we must discuss the definition of finite.

For any set $Z$, define $s(Z) = Z \cup \{ Z \}$. A set $I$ is called inductive if $\emptyset \in I$ and if, for all $Z \in I$, we also have $s(Z) \in I$. One can show (see any intro set theory book) that there is a unique set $\mathbb{N}$ such that (1) $\mathbb{N}$ is inductive and (2) every inductive set contains $\mathbb{N}$. A set $Y$ is called finite if it can be put in bijection with some member of $\mathbb{N}$.

We have now finished the definitions, and can move to the proof. We are going to show that, if $A \in \mathbb{N}$, if there is a bijection $Y \to A$, and if we have any map $\pi: X \to Y$ satisfying the hypotheses of CHOICE, then the conclusion of CHOICE holds.

First of all, composing $\pi: X \to Y$ with the bijection $Y \to A$, we may assume that $Y$ is an element of $\mathbb{N}$. (Exercise!)

Let's say that "we may make $Y$ choices" if CHOICE is true for $Y$, for all $\pi$ and $X$. Let $T \subseteq \mathbb{N}$ be the set of those elements $Y$ of $\mathbb{N}$ for which we can make $Y$ choices. (Exercise: Actually write out the definition of $T$ set theory notation.) We will show that $T$ is inductive.

First of all, we can make $\emptyset$ choices. Take $K = \emptyset$.

Now, suppose that we can make $Z$ choices. We must show that we can make $s(Z)$ choices. Consider any map $\pi: X \to s(Z)$. Let $X' = \pi^{-1}(Z)$, using the inclusion $Z \subseteq s(Z)$. So, by hypothesis, there is a subset $K' \subseteq X'$ such that, for every $y \in Z$, there is a unique element $x \in K'$ with $\pi(x) = y$. Also, by the hypotheses of AC, there is an element $x \in X$ such that $\pi(x) = \{ Z \}$. Take $K = K' \cup \{ x \}$.

We have now shown that $T$ is inductive, so $\mathbb{N} \subseteq T$. But also $T \subseteq \mathbb{N}$, by construction. So $T = \mathbb{N}$. We have shown that we can make $Y$ choices for every $Y \in \mathbb{N}$, as desired.

By the way, you may notice that this proof looks a lot like a proof by induction. This is how you write a proof by induction in ZF. Set theorists writing for a more experienced audience would just say "do it by induction", without all the explanation I've given.

-
By the way, does anyone have a recommendation for a set theory text book which does a lot of this sort of expansion of arguments in detail? I find that the gap because the ordinary language of set theory practitioners, and the formal definitions of the theory, is much larger than in any other field of math. I've gotten myself over the hump by now, but we frequently have questions here on whether something can be done in ZFC where the obstacle is just that the poster is not clear that an informally described argument can be formalized. –  David Speyer Sep 13 '11 at 20:08
How do you know that the class of ALL socks in the universe is a set? If we think of socks as pairs, then it is certainly not the case. –  Asaf Karagila Sep 13 '11 at 20:52
Interesting point. In terms of rigour, there is no issue: I am defining CHOICE to be the statement that surjections of sets have sections, which is one of the standard choices. But you're right, we could make choice be the following statement-schema: For any first order property $\Phi(x,y)$, and any set $Y$, if for all $y \in Y$, there is a set $x$ with $\Phi(x,y)$, then there is a set $K$ and a function $f: Y \to K$ such that, for all $y \in Y$, we have $\Phi(f(y), y)$. –  David Speyer Sep 13 '11 at 20:57
(continued) I sense the axiom of replacement floating in the background here. I didn't go this way because I didn't think of it but, even if I had, I wouldn't have gone this way because I don't want to talk about classes and statement-schemas if I don't have to. –  David Speyer Sep 13 '11 at 20:58
You don't need a schema for the axiom of choice, not even if you only want it for countable sets of pairs. It is a single assertion that says that the product of set many (or countably many, etc.) non-empty sets (sets with some property such as being pairs) is non-empty. This can be formulated in many other ways as well. –  Asaf Karagila Sep 13 '11 at 21:00

(Being somewhat harassed about notation issues, I am completely rewriting the answer)

Suppose $A=\{y_n\mid n\in\omega\}$, where $y_n=\{a,b\}$ for some $a,b$. Of course, $y_n\cap y_m=\varnothing$ to avoid trivialities.

We can define, by induction, a function from finite $n$ into $\bigcup A$ which chooses from the $n$-th pair.

For $n=0$ it is simple, $\exists a_0(a_0\in y_0\rightarrow f_0=\{\langle 0,a_0\rangle\})$.

Suppose we defined $f_n=\{\langle 0,a_0\rangle,\ldots,\langle n,a_n\rangle\}$, where $a_n\in y_n$. Now simply reiterate the above: $\exists a_{n+1}(a_{n+1}\in y_{n+1}\rightarrow f_{n+1} = f_n\cup\{\langle n+1,a_{n+1}\rangle\})$.

(This, of course, can be written purely with $\in$ and $=$. I am skipping extreme formality for sake of clarity.)

One can ask, if we defined this for all $n$, how come we cannot define $f=\bigcup f_n$ such that $f\colon\omega\to\bigcup A$ would choose from infinitely many pairs?

It is a good question. The answer lies on the fact that we do not specify the actual functions, but rather just assumed that the previous one existed. At the $n+1$-th stage, the $f_n$ from the induction hypothesis might be different from the one given at the $k$-th stage some other time.

The assertion that if we define $f_n$ for all $n$ then there exists a chain of infinite length is called The Principle of Dependent Choice, which is a fragment of the axiom of choice used often in analysis. When creating a model in which there exists an $A$ as above without a choice function, we create a model in which this choice principle does not hold (and in fact even less choice does not hold).

The proof by induction, however, still holds without the need for the axiom of choice. We can still write finite choice functions. How? Well, we simply "unfold" the proof by induction:

Suppose I want to choose 4 elements. Well, the proof says that if there is a choice of three elements I can choose a fourth one; if there exist a choice of two elements then I can choose a third one; and if there exists a choice of one element then I can choose a second.

One element I can always choose, simply because we know that the set is not empty. Let $a_0$ be some arbitrary element from $y_0$, now I roll upwards as the above sentence allows me and I choose $a_0,\ldots,a_3$ from $y_0,\ldots,y_3$ resp.

This method cannot be used to choose infinitely at a time because we chose arbitrary elements. Nothing guarantees that we will choose these elements again the next time. We could insist on $a_0$ to be chosen every time, and that $a_1$ is never chosen.

These constraints, if you will, need to be written down in a formula whose length is finite therefore cannot allow infinitely many choices without some function that does that in advance.

An important piece of information is that allowing a choice from countably many pairs of socks is still not enough for implying the axiom of choice. Not even if we allow any infinite set of pairs.

In fact, the above will not even imply that we can choose one finger from infinitely many hands.

It goes further. Much much further than that, and there is tangled web of implications of restricted versions of the axiom of choice, parts of it still lie in darkness awaiting to be discovered.

A sketch proof for such model using ZFA (ZF+Atoms).

Suppose $V$ is a model of ZFA+AC in which there are countably many atoms. Consider a partition of the atoms into countably many pairwise disjoint pairs. That is to say $A=\bigcup\{\{a_n,b_n\}\mid n\in\omega\}$.

Now take permutations of the atoms such that $\pi(\{a_n,b_n\})=\{a_n,b_n\}$, that is respect the partition into pairs.

Take a support ideal of finite sets, that is for some $k\in\omega$ we have that if $n<k$ then $\pi a_n=a_n$ (which also forces $\pi b_n=b_n$).

Consider $\mathcal U$ the permutation model created by these permutation and the ideal of supports described as above.

The sets of atoms is in $\mathcal U$, as well the partition into pairs (which is fixed by any permutation in our group). Any function which chooses from infinitely many pairs cannot have a finite support, there it does not exist in $\mathcal U$.

-
If you've named the socks $a_n, b_n$, you're already in the realm of shoes, not socks, and you can just specify $\{ a_0, a_1, a_2, a_3, ... \}$. You need to name the pairs, not the socks. –  Qiaochu Yuan Sep 13 '11 at 18:57
@Qiaochu: You'd be surprised, but no. I don't mind adding a sketch of a proof. It will probably, however, be above the head of the OP. –  Asaf Karagila Sep 13 '11 at 18:58
Huh. It seems to me that if you've named the socks the way you did, you already solved the problem that the OP wants to consider (finding a way to choose one out of each pair of the socks). Are you saying that you haven't? –  Qiaochu Yuan Sep 13 '11 at 19:04
@Qiaochu: The point is that you can identify the $n$-th pair, and within every pair you can identify $a_n$ and $b_n$. You can also do that within finitely many pairs, of course. You cannot, however, uniformly identify infinitely many $a_n$'s at one time. –  Asaf Karagila Sep 13 '11 at 19:07
@Asaf: if there isn't a function with domain $\mathbb{N}$ that maps $n$ to $a_n$, then I don't think $a_n$ has any business being called $a_n$. –  Chris Eagle Sep 13 '11 at 19:09

Although I'm sure an expert on this (which I'm not) will post a detailed explanation, here's a July 2006 sci.logic thread on what you're asking about:

3) Cf. Littlewood I, p. 14. As has been pointed out by Bernays (e.g., in 30, pp. 359f; cf. Hilbert-Bernays 34, p. 41), the assertion of the multiplicative axiom for finite sets $t$ is nothing but an application of one of the distributive laws connecting logical conjunction and disjunction. Hence in the general case one may conceive the axiom as a generalization of this elementary logical law to infinite sets; in other words, as a supplement to the logical rules governing general and existential statements. Cf. Collins 54. (Cf. the intuitionistic attitude to the principle of the excluded middle; see Chapter IV, [Section] 3.)