# Which axioms of ZF are used for finite choice?

Apologies if this is a silly question, not an expert in set theory but just wondering about it.

ZF implies finite choice. But let's suppose one wanted to work without it. The thinking here is being uncomfortable about sets where none of the elements are computable/definable, therefore one couldn't pick one explicitly. The idea is to allow nonempty sets where it's not allowed to pick exactly one element, you may be able to define subsets but not a single element. Obviously, finite choice is allowed when it's possible to constructively name an element.

Which axiom(s) of ZF would have to go in order to remove finite choice? Is there any set theory that rejects finite choice, or is this pruning away too many useful results?

• By speaking of definable elements, the question seems to conflate the question of whether there is a choice function with whether there is a computable/definable choice function. Even when elements are not definable, one can prove the existence of choice functions for finite families by induction on the size of the family. This is trivial if the family has only one set. If one adds a nonempty set to a family of $n$ nonempty sets, then every choice function on the previous family extends to the new family, one extension for each element of the newly added set. This uses very little of ZF. – Joel David Hamkins Aug 25 '14 at 17:15
• Since we use induction to prove finite choice, we need to somehow disallow induction. I suppose disallowing sufficiently many replacement/separation axioms will do the trick. But when you remove these axioms you really just get left with a very weak theory, not something I would call "set theory" in any serious meaning of the term. – Asaf Karagila Aug 25 '14 at 17:29
• What about Vopěnka's principle in this context? – მამუკა ჯიბლაძე Aug 25 '14 at 17:32
• @AsafKaragila Right. But notice also that you don't even need induction in the theory to prove the instances of AC for finite families, provided that the size of the family is finite in the meta-theory. That is, even without induction we can prove AC for families of size 1, size 2, size 3, and so on, as a theorem scheme. – Joel David Hamkins Aug 25 '14 at 17:40
• @Joel: But that's a big "provided". Since one can easily manufacture a model where this fails using compactness. Of course the failure is at non-standard finiteness, but still it makes finite choice unprovable (internally). – Asaf Karagila Aug 25 '14 at 17:41

As mentioned in the comments, one needs truly very few ZF axioms to prove the instances of of the axioms of choice for finite families. Let us denote by $\text{AC}\upharpoonright n$ the assertion that every collection $\cal A$ of $n$ nonempty disjoint sets has a selecting set $B$, that is, a set $B$ such that $A\cap B$ is a singleton for every $A\in\cal A$.

(Note that this is not the same as the assertion that every collection of disjoint sets of size $n$ has a selector.)

Part of the point now is that $\text{AC}\upharpoonright 0$ is basically vacuous, since the empty family has any set as a selector vacuously. Further, if $\text{AC}\upharpoonright n$ holds, then one may easily prove $\text{AC}\upharpoonright (n+1)$ as follows: given any family of size $n+1$, consisting of disjoint nonempty sets, we may delete an element $A$ from it and have a family of size $n$, which has a selector by the hypothesis, and this selector can be extended to a selector on the large family by adjoining any element of $A$. Thus, by induction, we prove $\text{AC}$ for all finite families.

Note that in the inductive step of the argument, we don't need to worry about defining a particular element of $A$, the set we deleted, since we are not proving that there is a definable selector; rather, we are only proving the existence claim that every such family has at least one selector. Similarly, we don't need to worry about how to choose a particular element to delete---the proof shows that for each set $A\in\cal A$, there are selectors obtained by deleting that set. So there is at least one selector.

Thus, by induction, we prove $\forall n\ \text{AC}\upharpoonright n$, or in other words, that the axiom of choice holds for finite families.

How much of ZF suffices for this argument? Of course we needed some very basic things like extensionality, pairing and union in order to make sense of the empty set and adjoining an element and so on, and perhaps one doesn't want to do set theory anyway without these axioms. Secondly, we needed to be able to prove a statement by induction on the natural numbers.

Thus, the argument can be undertaken in Kripke-Platek set theory, a very weak subsystem of ZF. One issue is that one might think that $\Sigma_2$-separation is required for the inductive argument, in order to form the set $\{ n\in\mathbb{N}\mid \neg \text{AC}\upharpoonright n\}$, with a view to proving that this set can have no least element, since the negation of $\text{AC}\upharpoonright n$ appears to be a $\Sigma_2$-assertion as it asserts the existence of a family of size $n$ with no selector. But KP includes the $\in$-foundation scheme, which allows one to prove statements of any complexity by $\in$-induction, and this implies natural-number induction.

But as noted, we really only needed natural number induction for $\Pi_2$-assertions, since $\text{AC}\upharpoonright n$ has complexity $\Pi_2$, and this would be a weakening of KP. I expect that one can go much lower than KP.

Lastly, as I mentioned in the comments, we don't need any induction scheme at all to prove every instance of $\text{AC}\upharpoonright n$ for meta-theoretically finite $n$, that is, to prove $AC$ for families of size $1$, of size $2$, of size $3$ and so on, as a theorem scheme. The reason is that for such meta-theoretically finite families, the induction can be undertaken in the meta-theory, rather than in the object theory, and so one needs hardly any set theory at all to prove these instances.