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{F}\mathrm{n}(\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 later. The natural argument "$A$ is infinite, so pick $a_0$, then $a_1$, and so on" uses a choice principle (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$) ↗). Once the symmetric-model construction is proved, this model will witness that such an extraction is not available in ZF. It also explains why Finite, countably infinite, countable, uncountable ↗ keeps ordinary and Dedekind finiteness distinct at the definitional level.

• 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.