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.

• In case you are still interested in answers to this old question, see the paper of Omar De la Cruz cited in the latest version of my answer.
– bof
Feb 10 at 9:57

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, 2021 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, 2021 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, 2021 at 21:38
• math.stackexchange.com/questions/3803247/… Feb 6 at 14:21

Let us write D-finite for Dedekind-finite.

The following statements are equivalent in ZF:
(1) Every D-finite set is finite.
(2) If $$\mathcal A$$ is a family of nonempty D-finite sets and $$|\mathcal A|\not\gt\aleph_0$$, then $$\mathcal A$$ has a choice function.
(3) Every D-finite family of infinite D-finite sets has a choice function.
(4) Every countable family of infinite D-finite sets has a choice function.

(1)$$\implies$$(2): We may assume that the family is infinite and therefore countable. If $$\{A_1,A_2,A_3,\dots\}$$ is a countable family of nonempty D-finite sets without a choice function, then $$\bigcup_{n=1}^\infty(A_1\times\cdots\times A_n)$$ is an infinite D-finite set.

(2)$$\implies$$(3)$$\land$$(4): Obvious.

(3)$$\implies$$(1): Assume (3), and assume for a contradiction that $$X$$ is an infinite D-finite set. Let $$S$$ be the set of all finite sequences of distinct elements of $$X$$, and for $$s\in S$$ let $$X_s=\{s\}\times(X\setminus\operatorname{range}(s))$$. Then $$S$$ is a D-finite set, and $$\{X_s:s\in S\}$$ is a D-finite family of infinite D-finite sets. By (3) this family has a choice function; but with such a choice function we can recursively define an infinite sequence of distinct elements of $$X$$, contradicting our assumption that $$X$$ is D-finite.

(4)$$\implies$$(1): If $$X$$ is an infinite D-finite set, let $$F_n=\{f\in X^n:f\text{ is injective}\}$$; then $$\{F_1,F_2,F_3,\dots\}$$ is a countable family of infinite D-finite sets without a choice function.

P.S. The equivalence (1)$$\iff$$(3) is essentially Theorem 17 of Omar De la Cruz, Finiteness and choice, Fundamenta Mathematicae 173 (2002), 57–76.

• Is this published anywhere? I think it's worth going on the Wikipedia page en.m.wikipedia.org/wiki/… as what is there is not backed up by a reference anyway, and citing here if nothing else Feb 3 at 0:37
• @theHigherGeometer Sorry, I don't know a reference. I've never seen these silly "choice principles" before; I just concocted them to answer this question. But I can't claim originality as I'm not well versed in the subject; for all I know they are standard textbook exercises.
– bof
Feb 5 at 8:54
• I'm glad I could prompt cleaning this up! Feb 5 at 23:42
• I'd strongly encourage you and Alex to write a two page note and send it to somewhere like PAMS. It's a small, easy, and should appear as a published result somewhere. Feb 6 at 14:21
• @AsafKaragila Alternatively, when you write a textbook you could include it as an exercise for the reader. But I take your comment as confirmation that my answer is correct, which I wasn't quite sure of. While the arguments are trivial, AC is so natural that it's easy to slip up and use it unawares. Thank you.
– bof
Feb 6 at 22:47