How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Dedekind infinitude is equivalent to a countable subset
Statement
In ZF the following are equivalent: is Dedekind-infinite; ; and . Equivalently, is Dedekind-finite iff . Here is the Hartogs number.
Facts & Assumptions
Dedekind-infinite and Dedekind-finite sets: Dedekind infinitude is witnessed by an injective nonsurjective self-map.
The recursion theorem: Iterates of a specified self-map form an omega sequence.
Hartogs: an ordinal that does not inject into a given set: An ordinal below embeds into , while does not.
Proof
Given: The objects and hypotheses in the statement.
For an injective nonsurjective , fix and put . If with , cancel repeatedly to get , impossible. Thus injects omega into .
Given an injection , send to , each to , and every other point of to itself. This is a bijection . Conversely, restricting any such bijection to is injective and misses the image of , proving Dedekind infinitude.
By the least-nonembedding definition, omega embeds into exactly when . Negating gives the asserted Dedekind-finite characterization. For finite , including the empty set, no injective nonsurjective self-map exists, as finite counting also shows.
Depends on
Used by
Dependency tree · two levels
13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Caicedo, Some choiceless results (3), §8 first theorem and proof (standard reference, not scraped)