How does the set of choice functions look like while proving the axiom of choice from ZF+Zorn’s lemma

Question

The usual proof of AC from ZF+Zorn’s Lemma starts as follows: Let $X$ be a nonempty set whose elements are all nonempty. Then define a partial on the set $\{ f:Y\rightarrow \bigcup X: Y\subseteq X, \; \forall y\in Y\; f(y) \in y\}$ as the usual set inclusion of functions. Then…

My question is that how does the defined set look like? I mean if some subset $Y$ of $X$ doesn’t have a choice function how do we know that a choice function of $Y$ is in the set. We don’t know AC yet. So the defined set contains “subsets of $X$ which already has a choice function”. But the antecedent of the Zorn’s lemma (intuitively speaking) somehow uses a fact for “any chain” of the corresponding set. What is the problem in my intuition?

Answer 1

Indeed, a priori there is no reason to think there should be an element of the poset of all partial choice functions for which $Y=X$ (that's why we need something like Zorn's lemma to prove AC, after all). However, we do note that any partial choice function that doesn't have $Y=X$ can easily be extended (for instance by adding a single element to its domain). So such a function cannot be maximal.

The crux of using Zorn's lemma is that it guarantees the existence of maximal elements in this poset. And maximal elements must necessarily be choice functions on all of $X$ by the above argument.

The reason we can apply Zorn's lemma in the first place (assuming we assume it) is that

1. The poset is non-empty (any singleton $Y$ trivially has a choice function)
2. Any chain of functions has an upper bound (the union of the functions in that chain)

Regarding point 2: We are not asked to prove the existence of any particular kind of chain. We don't need to construct any chains, or make sure that there are chains that eventually cover all of $X$. None of that. We only need to prove that whenever we do have a chain, it has an upper bound.

What makes Zorn's lemma as powerful (and as non-constructive) as AC is exactly that it takes that step from "Some chains exist" + "All chains have bounds" to "there are maximal elements" for us, just like AC takes the step from "Each set has an element" to "There are functions that choose an element from each set".

Answer 2

$\mathsf{ZF}$ does not prove that every family of nonempty sets has a choice function, but it does prove that every finite family of nonempty sets has a choice function. For example, if we have a family $Y=\{y_1,\dots,y_n\}$ of nonempty sets, then the formula $$\exists v_1\cdots\exists v_n(v_1\in y_1\land\cdots\land v_n\in y_n)$$ is valid, simply because we have defined all sets to be nonempty. Since this formula is valid, we can use existential instantiation to find sets $x_1,\dots,x_n$ such that $(x_1\in y_1\land\cdots \land x_n\in y_n)$ is valid, and thus the function $f=\{\langle y_i,x_i\rangle\mid 1\leq i\leq n\}$ can be constructed.

The same does not work for infinite families of sets, since we would need to instantiate infinitely many existential quantifiers, something which is not allowed (proofs are finite after all).

---

Now, if $Y$ is an infinite set, we can partition it into singletons $\{\{y\}\mid y\in Y\}$, and for each $\{y\}$ there exists a choice function $f_y:\{y\}\to y$ by the above reasoning. If a choice function $f$ with domain $A\subset Y$ exists, and $y\in Y\setminus A$, then clearly $f\cup f_y$ is also a choice function and it is larger than $f$ in the partial order defined on the choice functions. So, when $f$ is a maximal element of some chain $C$, then the domain of $f$ must equal all of $Y$ (or we can extend $C$ with $f\cup f_y$ for some $y\in Y$ outside of $\mathrm{dom}(f)$).

Of course, Zorn's lemma is not constructive, and neither is existential instantiation. Therefore we don't get a method by which we pick elements; it only shows that we can pick some element in every non-empty set, but not which element.