Context for Russell's Infinite Sock Pair Example 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?
 A: 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:

Is there a formula $\phi(x)$ such that

*

*ZFC proves that exactly one $x$ satisfies $\phi$,

*ZFC proves that every element of $x$ has cardinality $2$, but

*ZFC does not prove for any $\psi(y,z)$ that $\{ (y,z) \mid y\in x, z\in y, \psi(y,z) \}$ is a choice function on $x$?


A: Existence is not a predicated property. It is a semantic property.
What does it mean? It means that after you've fixed a universe of set theory, there are things which exists there, and that's that. They don't have to be defined a-priori in order to exist, and they don't have to have a definition either in order to exist. They just do.
It is consistent with the failure of the axiom of choice that there is a family of pairs without a choice function. That is a mathematical theorem which tells you that it is possible to have a universe of set theory in which there is a set which can be partitioned into countably many pairs without a choice function.
We don't create anything. If anything is "created" it means, generally, that we proved its existence from the axioms, which implies that we can always find that set which was created (or its likened image). And of course we cannot prove from $\sf ZF$ that there is always such set. In fact, even if we assume that there is a set which cannot be linearly ordered we still cannot prove that there is a countably family of pairs without a choice function.
