TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-06 (claude-opus-5)

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.

There is no $R$ with $x \in R \leftrightarrow x \notin x$ for every $x$

Statement

There is no set $R$ such that, for every set $x$ ,

$x \in R \leftrightarrow x \notin x .$

Facts & Assumptions

Given: the language of set theory, in which $x \in R$ and $x \notin x$ are formulas (The first-order language of set theory: $\in$ , $=$ , formulas with parameters, and class abbreviations).

Proof

technique · contradiction

1.1

Suppose there is a set $R$ such that $x \in R$ holds if and only if $x \notin x$ , for every set $x$ .

assume-contra

2.1

The hypothesis holds for every set $x$ , and $R$ is a set, so it holds for $x : = R$ : $R \in R$ if and only if $R \notin R$ .

step 1.1

3.1

A statement equivalent to its own negation is contradictory: if $R \in R$ then $R \notin R$ , and if $R \notin R$ then $R \in R$ , so each alternative refutes itself. There is therefore no such $R$ .

step 2.1discharge-contradiction∎

Remarks

What fails is unrestricted comprehension, not a particular formula. The argument uses only that $x \notin x$ is a formula of the language and that the supposed $R$ is itself a set, so it refutes any principle asserting that every formula has a set of all its instances. Separation and Replacement build subsets of sets already in hand, which is exactly what blocks Russell's construction records how The Axiom Schema of Separation: for each formula $φ$ , $\forall \overset{ˉ}{p} \forall x \exists y \forall z (z \in y \leftrightarrow (z \in x \land φ (z, \overset{ˉ}{p})))$ avoids it.

Depends on

The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations

Used by

Dependency tree · one level

1 result within one dependency step 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

Russell's paradox (Wikipedia) (standard reference, not scraped)
B. Kaya, MATH 320 Set Theory (METU), Theorem 3 (standard reference, not scraped)
Zermelo-Fraenkel set theory (Wikipedia) (standard reference, not scraped)

There is no RR with x∈R↔x∉xx∈R↔x∈/x for every xx