Understanding choice functions - Teichmüller-Tukey Proof

Question

There is a proof that the Teichmüller-Tukey lemma implies AC that seems to work in the following way:

1. Let $\mathcal{F}$ be any family of nonempty sets.
2. Consider $\mathcal{E}$={$f$: $f$ is a choice function for some subfamily $\mathcal{F}'\subseteq \mathcal{F}$}
3. Since $f$ is a choice function if and only if every finite subfunction is a choice function, $\mathcal{E}$ has finite character.
4. Therefore, by Teichmüller-Tukey lemma, $\mathcal{E}$ has a maximal element, say $f_{\max}$.
5. Since $f_{\max}$ is maximal, we have $\operatorname{dom}(f_{\max})=\mathcal{F}$. Hence, $f_{\max}$ is a choice function of $\mathcal{F}$.

Now, my question is:

How can we consider the set of partial choice function without knowing that there are choice functions?

Extra question:

How can we define a choice function on finite families of sets without the axiom of choice?

Answer 1

First of all, note that there are always lots of partial choice functions on any family of nonempty sets: the empty function is always a partial choice function (:P), and less trivially if we fix a single set $A$ in the family and a single element $a$ of $A$, the function $\{(A, a)\}$ - with domain $\{A\}$, sending $A$ to $a$ - is a partial choice function.

But regardless, we don't need to know that a set is nonempty in order to consider it. Take any family $\mathcal{F}$ of nonempty sets; then ZF (indeed, much less) proves that there is a set $C$ consisting of all choice functions on $\mathcal{F}$. ZF does not prove, in general, that $C$ is nonempty; but it does prove that $C$ exists.

---

As to proving finite choice, this is a nice argument. By induction on finite $n$, ZF proves: "For all finite $n$, every family of $n$-many nonempty sets has a choice function." The induction goes like this:

• The base case is trivial.

• Now suppose $\mathcal{F}$ is a set of $(n+1)$-many nonempty sets, and every family of $n$-many sets has a choice function. Fix some $A\in\mathcal{F}$ and let $\mathcal{G}=\mathcal{F}\setminus\{A\}$. Then $\mathcal{G}$ has a choice function (by the induction hypothesis); pick a choice function $g$. Now fixing some $a\in A$, let $f=g\cup\{(A, a)\}$ (that is, $f$ extends $g$ to all of $\mathcal{F}$ by sending $A$ to $a$); it's easily checked that $f$ is a choice function.

The key to this proof is in the steps: "fix some $A\in\mathcal{F}$" and "fixing some $a\in A$." One of the rules of first-order logic is existential instantiation; we may always make, as a step in a proof, a single choice from some set we've proved is nonempty. So what's going on here is: in order to prove finite choice in ZF, we've used the fact that the rules of first-order logic allow us to make two choices in the course of a proof (namely, the choices of $A$ and $a$ above). In a sense, we could say that finite choice is built into first-order logic; this is missing an important point (see below), but isn't a bad first intuition.

This suggests, by the way, that we can view (versions of) the axiom of choice as representing a logical rule beyond the usual rules of first-order logic. Interestingly, this isn't the only time this crops up: axioms of determinacy can also be so viewed. Roughly speaking, saying "Every game on $X$ is determined" is equivalent to saying $$\forall x_1\exists x_2\forall x_3\exists x_4 ...[P(x_1x_2x_3x_4...)]\quad\vee\quad\exists x_1\forall x_2\exists x_3\forall x_4 ...[\neg P(x_1x_2x_3x_4...)]$$ where the quantifiers range over $X$, whenever $P$ is a property of sequences of elements of $X$. And this is sort of an "infinitary" version of De Morgan's laws for quantifiers.

Fascinatingly, even when we take $X=\{0, 1\}$ the resulting determinacy principle contradicts the axiom of choice; and the statement "determinacy holds for all sets $X$" is outright disprovable in ZF. So there's an interesting tension between some plausible logical rules beyond first-order logic. If I recall correctly, this is treated somewhat at the end of Takeuti's book on proof theory, but it's been a while since I read it and I don't have it on me.

---

Now let me say a bit about why the slogan "ZF proves finite choice since finite choice is built into the rules for first-order logic" is actually missing an important point:

Remember that saying "ZF proves $\varphi$" means "$\varphi$ is true in every model of ZF" (this is the completeness theorem). Now when we express finite choice in ZF, the word "finite" gets interpreted: any model of ZF has a collection of things it thinks are the natural numbers, and "finite" for that model means "in bijection with some finite natural number" from the point of view of that model.

But there are models of ZF which "get the natural numbers wrong." In such a model, there will be a collection of nonempty sets $\mathcal{F}$ which the model thinks is finite but is not actually finite. But since ZF proves finite choice, there will be a choice function for that family in the model, even though that family isn't really finite. So what's actually going on is that somehow external finite choice being built into first-order logic means that internal finite choice - a stronger principle - is provable in ZF. This ultimately is a kind of "overspill" argument, and diving too deep into what's going on here would take us well astray; but it's important to note that the short slogan I gave above isn't really the whole picture.

Answer 2

The empty set is a choice function from the empty family, which is a subfamily of $\cal F$.

Moreover, if $f$ is a partial choice function and $A\in\mathcal F\setminus\operatorname{dom}(f)$, then given any $a\in A$, we get that $f\cup\{(A,a)\}$ is also a choice function from a subfamily of $\cal F$.

This argument is not only the key to proving that any finite family of non-empty sets admits a choice function, but also in proving that a maximal element of $\cal E$ is necessarily a choice function from the entire family $\cal F$.