Dedekind-infinite characterization 2026-10-31
In ZF, an injection yields an injective nonsurjective self-map by shifting to and fixing the complement. Conversely, if an injection omits , the natural-number recursion theorem defines . Any repetition would, after cancellation, put in the image of . Thus is injective. The argument uses no axiom of choice, even when some infinite sets are Dedekind-finite sets.
Finite repetition-free sequences preserve Dedekind-finiteness Created 2026-10-05 Updated 2026-10-31
If is a Dedekind-finite set, its set of finite repetition-free sequences is also Dedekind-finite. An injective sequence of distinct finite lists would, by countable union of explicitly ordered finite lists without choice, either produce an injection or use only finitely many entries. The latter possibility is impossible because a fixed finite pool supports only finitely many repetition-free lists. If is infinite, the one-entry lists also show that the resulting set is infinite.