Choice function for collection of arbitrary finite sets. AC required?

I understand how we can show the existence of a choice function for any (finite or infinite) collection of (finite or infinite) subsets of, say, $\mathbb{N}$ or $\mathbb{Z}$ without using the axiom of choice, by showing that a well-ordering over the union of sets in the collection exists.

What I don't see though is how to do the same for what appears to be a much simpler case: a (possibly infinite) collection of finite sets, where nothing else is said about the sets other than that each of them is finite.

I would need to show a well-ordering exists over the union of those sets, but since they were not explicitly defined to be subsets of $\mathbb{N}$ or $\mathbb{Z}$, I first need to show the following, for example:

(i) there exists a surjection from $\mathbb{N}$ to $\bigcup X_i$ for an arbitrary collection of finite sets $X_i$

Correct so far?

Alternatively, I'm on the wrong track, and this is precisely a case that (unintuitively for me then) requires application of the axiom.

If so, I suppose I don't see why (i) wouldn't hold, when it seems that any definition within ZF of a finite number of elements is equivalent (in some sense to be made precise) to a finite subset of $\mathbb{N}$, so, given that the union of a collection of finite subsets of $\mathbb{N}$ is a subset of $\mathbb{N}$, the required well-ordering exists.


You're right. The axiom of choice is needed, albeit in a limited form.

It is consistent that there is a countable collection of pairs, $P_n$ such that there is no choice function from the $P_n$'s themselves. In particular, $\bigcup P_n$ is not a countable set, and in fact cannot even be linearly ordered.

But since it is consistent with $\sf ZF$ that the axiom of choice holds, we can't really give a proper and concrete definition for such a set. We can just prove that if $\sf ZF$ is consistent, then there is a model of $\sf ZF$ in which that happens, and other models of $\sf ZF$ in which it doesn't.

(By the way, you probably wanted to say that $\bigcup_i X_i$ is a countable union of finite sets; otherwise it's not true in $\sf ZFC$ either. Just look at $X_i=\{i\}$ for $i\in\Bbb R$, then $\bigcup_{i\in\Bbb R}X_i=\Bbb R$ and there is no surjection from $\Bbb N$ onto $\Bbb R$.)


This is closely related to König's lemma, which is equivalent in ZF to a choice principle for countable collections of finite sets. The Wikipedia article for König's lemma has a couple references. Quoting Wikipedia,

In particular, when the branching at each node is done on a finite subset of an arbitrary set not assumed to be countable, the form of König's lemma that says "Every infinite finitely branching tree has an infinite path" is equivalent to the principle that every countable set of finite sets has a choice function