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). 
 A: 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.
A: (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$.
A: 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:
http://groups.google.com/group/sci.logic/browse_thread/thread/e1e4adefec0be32a
Incidentally, I've read that the Axiom of Choice for finite collections is essentially due to the distributivity of "and" over "or" in logic.
Below is footnote 3 on p. 49 (Chapter II.4.2) of Foundations of Set Theory by Abraham A. Fraenkel and Yehoshua Bar-Hillel, North-Holland Publishing Company, 1958:
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.)
There is an English translation of the relevant Bernays paper freely available on the internet, and you can find Bernays' observation about AC and distributivity on pp. 47-48 of this translation:
http://www.phil.cmu.edu/projects/bernays/Pdf/bernays09_2002-07-26.pdf
