FALSE: every infinite set has a countably infinite subset, in ZF

FALSE. The statement

every infinite set has a countably infinite subset

is a theorem of ZF: it can be proved from the Zermelo-Fraenkel axioms without any choice principle.

Here "infinite" means "not finite" and "countably infinite" means "equinumerous with $\mathbb{N}$" (Finite, countably infinite, countable, uncountable, Equinumerous sets, $A \approx B$ and $A \preceq B$). The claim is plausible because the proof everyone reaches for seems to need nothing at all: $A$ is infinite, so it is nonempty, so pick $a_0 \in A$; then $A \setminus \{a_0\}$ is still infinite, so pick $a_1$; and so on, giving $\{a_0, a_1, a_2, \dots\} \approx \mathbb{N}$. The "and so on" is the whole difficulty. Each step depends on the previous choices and there are infinitely many of them, so what the argument uses is dependent choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$) records where DC sits), not a construction. Nothing in ZF turns "$A$ is not equinumerous with any natural number" into a rule for naming elements of $A$.

• What is and is not proved here. As in FALSE: Zorn's lemma is a theorem of ZF and FALSE: countable unions of countable sets are countable is a theorem of ZF, the refutation is conditional on the consistency of ZF and rests on an independence result that this library does not prove. The honest reading is: $S$ is a theorem of ZF only if ZF is inconsistent.

• With $\mathrm{AC}_\omega$ the statement is true, which is exactly why it feels obvious. This standard contrast is not proved in this library either. Given an infinite $A$, for each $n$ the set of injections $n \to A$ is nonempty, and $\mathrm{AC}_\omega$ selects one for every $n$ at once; from that sequence a countably infinite subset is assembled with no further choices. The intuition behind the naive argument is therefore not wrong, it is just not a ZF argument.

• Two notions of infinite come apart in ZF. A set is Dedekind-infinite when it is equinumerous with a proper subset of itself, equivalently when it has a countably infinite subset. Dedekind-infinite implies infinite in ZF, and that direction is a theorem of this library rather than a convention: it is claim 5 of The pigeonhole principle on $\mathbb{N}$, transported along a bijection. In detail, suppose $A$ were both finite and Dedekind-infinite, say $f : A \to n$ is a bijection onto a natural number and $g : A \to B$ is a bijection onto a proper subset $B \subsetneq A$. Then $f[B] \subseteq n$, and $f[B] \neq n$ because $f$ is injective and $B \neq A$, while $n \approx A \approx B \approx f[B]$; so $n$ is equinumerous with a proper subset of itself, which claim 5 forbids. The converse implication, that infinite implies Dedekind-infinite, is exactly $S$. So ZF does not prove the two notions equivalent, unless ZF is inconsistent: that separation is the conditional conclusion of the refutation above and inherits its consistency hypothesis, and an amorphous set, one that cannot be split into two infinite pieces at all, is infinite in the weak sense only.

• This is the reason the library's definition of finiteness (Finite, countably infinite, countable, uncountable) is by equinumerosity with a natural number rather than by the Dedekind condition. The two definitions are equivalent under $\mathrm{AC}_\omega$ and not equivalent in ZF, and only the first supports the induction arguments used in Every subset of an at most countable set is at most countable and The nonempty finite subsets of $\mathbb{R}$ are exactly the listable ones.