# What form of choice is "every Dedekind-finite set is finite" equivalent to?

Halmos in his Naive Set Theory proves that every infinite set has a subset equivalent to $$\omega$$ using the axiom of choice with its full power. And this leads to the corollary that a set is infinite if and only if it is equivalent to some proper subset of it, which leads to each Dedekind-finite set being finite.

But I've also seen a proof (on Wikipedia) that this can also be proven with just countable choice. However Wikipedia also states that this result is strictly weaker than countable choice.

Question: It is clear that we do require some form of choice, not just ZF, to prove this result.$$^1$$ But it is even weaker than the countable choice. Can we explicitly state the form of this choice which is equivalent to this result?

$$^1$$ I've come across the fact that there exists a model of ZF (whatever that means (sorry I've not done any model theory; this is just for your reference)) in which every infinite set is Dedekind-infinite, and yet the countable choice fails.

While answering this question: Strength of “Cofinite Choice”, I discovered that "every Dedekind-finite set is finite" is equivalent to the following "axiom of cofinite choice":

Let $$A$$ be a set of non-empty sets such that $$(\bigcup A)\setminus X$$ is finite for all $$X\in A$$. Then $$A$$ has a choice function.

See the linked answer for a proof. This seems to me to be a fairly natural choice principle.

• Eh, I'd argue about its being natural. Even the OP there suggested that the choice principle came out of trying to prove that an infinite set is Dedekind-infinite. Jan 14 at 21:23
• @AsafKaragila I guess it depends what you mean by natural. I just meant that the condition of being cofinite subsets of a given set is a fairly natural condition to impose on a family of sets. And it makes some intuitive sense that if the sets in the family are all "large" in some sense, then it should be easier to find a choice function... Jan 14 at 21:31
• @AsafKaragila That's not quite what I meant with it arising from the definition of the $f_n$, actually, I noticed a structure equivalent to these sets/choice functions has a few applications, which made me wondered whether these existed in general Jan 14 at 21:38

There's no "nice form of choice".

This follows from countable choice, but it is weaker. And it does not follow from less than countable choice. In fact, it implies countable choice from families of finite sets, which is arguably the strongest you can do below countable choice.