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.
Under Foundation, for every set , there are no sets with , and there are no sets with
Statement
Assume the Axiom of Foundation. Then:
- (i) for every set ;
- (ii) there are no sets and with and ;
- (iii) there are no sets , and with , and .
Cycles of length greater than three are not treated here: stating "there is no membership cycle of any finite length" needs a finite sequence, that is a function on a natural number, and neither notion is available at this point in the reading order.
Facts & Assumptions
Given: the Axiom of Foundation.
Every set with at least one member has a member that shares no member with it (The Axiom of Foundation: ).
is the set whose elements are exactly and , and (The unordered pair and the singleton ).
holds if and only if or (, , , , and ).
Proof
Suppose the statement fails, so that at least one of the following holds: there is a set with ; there are sets and with and ; there are sets , and with , and .
Suppose and put . Its only member is , so has a member and Foundation applies; the member it supplies must be , so shares no member with . But and , so is a member of both.
Suppose and , and put . Foundation supplies a member of sharing no member with , and that member is or . If it is , then and make a member of both; if it is , then and make a member of both.
Suppose , and , and put , whose members are exactly , and . Foundation supplies a member of sharing no member with . If it is , then and ; if it is , then and ; if it is , then and . In each case that member shares a member with .
Each of the three suppositions contradicts the member Foundation supplies, so none of them holds: for every , no sets satisfy , and no sets satisfy .
Depends on
- The Axiom of Foundation: $\forall S\,(\exists t\,(t \in S) \to \exists s\,(s \in S \wedge \neg\exists u\,(u \in s \wedge u \in S)))$
- The unordered pair $\{x,y\}$ and the singleton $\{x\} = \{x,x\}$
- The union $\bigcup x$ of a set, and the binary union $a \cup b := \bigcup \{a,b\}$
- $\bigcup \varnothing = \varnothing$, $\bigcup \{a\} = a$, $\bigcup \{a,b\} = a \cup b$, $\bigcap \{a\} = a$, and $\bigcap \{a,b\} = a \cap b$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 12 results over 6 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
- B. Kaya, MATH 320 Set Theory (METU), Theorem 11 and Exercise 24 (standard reference, not scraped)
- Axiom of regularity (Wikipedia) (standard reference, not scraped)
- Zermelo-Fraenkel set theory (Wikipedia) (standard reference, not scraped)