I wanted to verify the following considerations on the context of Russell's infinite sock pair conundrum. The conundrum pointed out that a rule for choosing from pairs of shoes is possible a-priori. For indistinguishable socks, such rule is not possible a-priori, and has to be assumed.
Thus, in Set Theory there are two major avenues for context of Russell's Sock Pair example for the role of Infinite Choice (choice from an infinite number of unordered pairs).
In the first situation the pairs arise from the set {1,2} acting on some set in repeated fashion. In this case, there is an ordering of the pairs, and choice is not needed. Alternatively, the set of pairs may arise from an linearly ordered set (e.g. set of pairs of elements of $\Bbb R$). In such case a well order can be defined on each pair a-priori. In such situations Russell's conundrum does not apply (the pair of shoes situation).
For Russell's sock pair conundrum to arise one needs a set of pairs drawn by comprehension from the powerset of an not totally ordered (t.o.) set. Use of replacement schema to create the pairs (but not to change an already existing collection to something else) would lead to the first situation (existence of an ordering approach).
Is this correct? is there any other (non-equivalent) path to get to the infinity of sock pairs beyond comprehension acting upon a non-t.o. set?
There's no definite way to create a set of sock pairs that don't admit a choice function, using the usual constructions allowed in set theory. After all, it is known that the Axiom of Choice is consistent with the usual axioms of set theory, meaning that it cannot be proved that such at sock set exists at all -- and an explicit construction of one would certainly count as an existence proof.
It is also consistent with ZFC that there is a single formula that always picks out one sock from each pair, and which works no matter which set you apply it to. (For example, if $V=L$ then there's a particular formula that well-orders the entire universe).
So the best you can hope for is a particular description of a definite set of pairs, such that no formula can be proved in ZFC to pick out one sock from each pair. I don't know for sure whether that is possible, though I would intuitively expect $$ \{\{(x,y),(y,x)\} \mid x\subseteq \mathbb R, y\subseteq \mathbb R, x\ne y \}$$ to be an example.
So a more precise question would be: