Cohen's first model: an infinite Dedekind-finite set of reals

If ZF is consistent, then ZF is consistent with the existence of a set $A \subseteq \mathbb{R}$ that is infinite and Dedekind-finite: $A$ is not equinumerous with any natural number, yet $A$ has no countably infinite subset, equivalently $A$ is not equinumerous with any proper subset of itself.

This is the model Cohen produced first, in 1963. Adjoin a countable family $(a_n)_{n \in \mathbb{N}}$ of mutually generic Cohen reals to a countable transitive model of ZFC, and pass to the symmetric submodel determined by finite supports and the full permutation group of the indices. In that submodel the set $A = \{a_n : n \in \mathbb{N}\}$ exists, but the sequence $n \mapsto a_n$ does not: a hereditarily symmetric name for an injection $\mathbb{N} \to A$ has a finite support $E$, and a permutation of the indices fixing $E$ but moving some index outside $E$ then fixes the injection while moving one of its values, which is impossible. So $A$ is infinite and has no countably infinite subset in the model.

• Not proved in this library. The symmetric-extension construction is not developed here; the description above is a statement of what is built, not a construction carried out.

• What would prove it. Forcing with finite partial functions $\mathrm{Fn}(\mathbb{N} \times \mathbb{N}, 2)$, the automorphism action on names, and the finite-support symmetric submodel, together with the standard genericity argument showing that no name for an injection $\mathbb{N} \to A$ is hereditarily symmetric. That is the same forcing track named in Cohen 1963: ZF does not prove the Axiom of Choice ‡.

• Why it matters here. It is the external fact that FALSE: every infinite set has a countably infinite subset, in ZF ↗ quotes. Without it, the natural argument "$A$ is infinite, so pick $a_0$, then $a_1$, and so on" looks like a ZF proof, and the failure is invisible: what the argument uses is a choice principle (The Axiom of Countable Choice ($\mathrm{AC}_\omega$) ↗), and this model is the witness that it cannot be removed. It is also the reason this library defines finiteness by equinumerosity with a natural number rather than by the Dedekind condition (Finite, countably infinite, countable, uncountable ↗): the two definitions part company in ZF.

• Conditional discipline. As always, the statement is an implication between consistency statements. This library never asserts that an infinite Dedekind-finite set exists, only that ZF cannot rule one out unless ZF is inconsistent.