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?

  • $\begingroup$ The extra question is a duplicate that was asked so many times before on this site. (And in any case, avoid "extra questions".) $\endgroup$ – Asaf Karagila Nov 4 '17 at 19:22
  • $\begingroup$ @AsafKaragila I see, this was not the best structure of a question. $\endgroup$ – GottlobtFrege Nov 4 '17 at 19:46

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.

  • $\begingroup$ Thank you very much! That was very helpful and interesting! Just two questions: In the base case of the induction you already use the principle you're explaining after - we pick an element of the non-empty only set of the family by existential instantiation (by knowing it to be non-empty)? Considering the non-standard models: How would you define "true finiteness"? Considering that these sets would be finite in the model but "not actually finite",. $\endgroup$ – GottlobtFrege Nov 4 '17 at 18:47
  • $\begingroup$ @GottlobtFrege "In the base case of the induction you already use the principle you're explaining after - we pick an element of the non-empty only set of the family by existential instantiation (by knowing it to be non-empty)?" No - in the base case, and in the induction step, we use the logical rule of existential instantiation. All we need to apply this to a set $x$, is the knowledge that $x$ is nonempty: in the course of a proof, if we have already proved that $x$ is nonempty, then we may introduce a new symbol standing for an element of $x$ (that is, pick an element of $x$). (cont'd) $\endgroup$ – Noah Schweber Nov 4 '17 at 18:55
  • $\begingroup$ @GottlobtFrege "Considering the non-standard models: How would you define "true finiteness"? Considering that these sets would be finite in the model but "not actually finite"" Inside a model of ZF, all we can do is define what that model thinks "finite" means. When we talk about "true" finiteness, we do some from the point of view of some "true" universe of sets. (That's the Platonist take; we can make this purely formalist of course, but understanding the Platonist view is a good first step in my opinion: while I find Platonism hard to defend, it's a useful conceptual tool.) $\endgroup$ – Noah Schweber Nov 4 '17 at 18:57
  • $\begingroup$ I can promise you that finding all the duplicates and related questions on finite choices would have taken less time than typing the whole thing. $\endgroup$ – Asaf Karagila Nov 4 '17 at 19:26
  • $\begingroup$ @AsafKaragila I actually wasn't completely satisfied with any of the answers I found; I really wanted one that both gave the slogan "finite choice is provable in ZF since it's built into first-order logic" and went into the subtleties of that slogan. Since I couldn't find one, I made one. (Also, any excuse to reference Takeuti is a good one.) $\endgroup$ – Noah Schweber Nov 4 '17 at 19:42

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$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.