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.
Separation and Replacement build subsets of sets already in hand, which is exactly what blocks Russell's construction
Remark
An unrestricted comprehension principle would assert, for every formula of the language (The first-order language of set theory: , , formulas with parameters, and class abbreviations), that . Taking turns that assertion into precisely the set There is no with for every shows cannot exist, so the principle is refutable in plain first-order logic; no appeal to any axiom below is needed to reject it.
The Axiom Schema of Separation: for each formula , asserts something weaker in a specific way: it does not produce a set from a formula alone, but only from a formula together with a set already in hand, and the set it produces is a subset of that . Running Russell's argument against it therefore yields no contradiction but a theorem. Given any set , the separated set exists; asking whether shows that is impossible, since would give . So every set has a subset that is not one of its elements, and no set contains every set, which is There is no set with for every set .
The same restriction is what makes The Axiom Schema of Replacement: for each formula , if defines a class function on then its image on is a set safe. It does not assert that an arbitrary class is a set either: its hypothesis is that a formula behaves like a function on a set already in hand, and its conclusion is about the image of that particular set. Both schemas therefore build only from material already given, and neither can be turned on the universe at large.
What is given up is small and is worth naming exactly: from these axioms alone nothing whatever can be constructed, which is why The Axiom of Infinity: there is a set containing a set with no elements and closed under is assumed outright rather than derived, and why There is exactly one set with no elements, written needs the logical fact that the domain of discourse is nonempty before Separation has anything to act on.
Depends on
- There is no $R$ with $x \in R \leftrightarrow x \notin x$ for every $x$
- There is no set $U$ with $y \in U$ for every set $y$
- The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$
- The Axiom Schema of Replacement: for each formula $\varphi$, if $\varphi$ defines a class function on $A$ then its image on $A$ is a set
- The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations
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: 7 results over 4 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
- Russell's paradox (Wikipedia) (standard reference, not scraped)
- Zermelo-Fraenkel set theory (Wikipedia) (standard reference, not scraped)
- B. Kaya, MATH 320 Set Theory (METU), §1.1 and Axiom 5 (standard reference, not scraped)