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.
FALSE: the ordinals form a set
Statement
FALSE. The ordinals (Ordinal (von Neumann)) form a set: there is a set whose members are exactly the ordinals.
The claim is plausible because the ordinals look locally set sized. Every ordinal is itself precisely the set of all ordinals below it, so every downward closed collection of ordinals that stops somewhere is a set, and it is tempting to conclude that the collection of all of them is a set as well. In ZF that inference is unavailable: Separation produces a set only as a subset of a set already in hand, and here there is no such ambient set to start from.
Facts & Assumptions
Given: The axioms of ZF, in particular Separation. No choice principle is used.
Separation carves a subset out of a set already given; it never produces a set from a defining property alone.
No set has every ordinal as a member (Burali-Forti: there is no set of all ordinals).
Every element of an ordinal is an ordinal, and no ordinal is a member of itself (Basic closure properties of ordinals).
An ordinal is a transitive set on which is a strict well-order, and means (Ordinal (von Neumann)).
Refutation
Suppose the claim: there is a set whose members are exactly the ordinals.
The source of the intuition is genuine but limited: by [L3] and [L2] each ordinal equals , so every collection of ordinals bounded above by some ordinal is a set, being a subset of that bound; by [A1] this says nothing about the unbounded collection of all ordinals.
Under the supposition, is a set having every ordinal as a member.
No such set exists: it would be transitive by [L2], since every element of an ordinal is an ordinal and so a member of it, and would strictly well-order it, so it would itself be an ordinal by [L3] and hence a member of itself, which [L2] forbids; this is exactly [L1].
Steps 2.1 and 3.1 are contradictory, so no set has the ordinals as its members: the ordinals form a proper class and the claim is false.
Remarks
Bounded is not unbounded. The honest version of the intuition is: for every ordinal , the ordinals below form a set, namely itself. Nothing in ZF upgrades a family of sets indexed by a proper class into one set, and the attempt to do so here is exactly what Burali-Forti: there is no set of all ordinals refutes.
The same trap, one level up. "The sets form a set" fails for a closely related reason, and "the cardinals form a set" fails because the cardinals (Cardinal (initial ordinal) and cardinality) are unbounded among the ordinals. In each case the correct statement replaces "set" by "proper class", which in ZF means a formula rather than an object.
What is still available. Nothing about the theory of ordinals needs them to form a set. Every construction on this page indexes by a set of ordinals, or by a single ordinal, or runs along an arbitrary well-order; Transfinite recursion and Hartogs: an ordinal that does not inject into a given set are both stated so that only sets are ever formed.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 20 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Burali-Forti paradox (Wikipedia) (standard reference, not scraped)
- Ordinal number (Wikipedia) (standard reference, not scraped)
- A. Marks, Set Theory (standard reference, not scraped)