Mathematical logic and foundations Proof
Proof of Russell's paradox
Proof
We argue by contradiction.
- Suppose that there is a set such that, for each set , if and only if .
- The object is itself a set. So we may take in step 1. This gives: if and only if .
- Suppose . By step 2, . This contradicts the assumption .
- So is false, that is, is not an element of . In symbols, .
- By step 2 and step 4, .
- Steps 4 and 5 give both and , a contradiction.
- So the assumption of step 1 is false. There is no set such that, for each set , if and only if .
Idea
Ask whether contains itself. The defining property of says that exactly when . No statement can be equivalent to its own negation, so no such exists.
Reading path
To understand this page from the ground up, read these 3 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Element definition
- Set definition
- Proof of Russell's paradox proof
Where this leads
45 pages build on this one.
- Russell's paradox
- Simply typed lambda calculus
- Type system
- Type theory
- Naive set theory
- Parametricity
- Constructible universe
- Hindley–Milner type system
- Calculus of constructions
- Univalence axiom
- Curry–Howard correspondence
- Hindley–Milner type system
- Type safety
- Univalence axiom
- Girard's paradox
- Inductive type
- Type inference
- Homotopy type theory
- Intuitionistic type theory
- Zero sharp
- Parametricity
- Subtyping
- Homotopy type theory
- Calculus of inductive constructions
- Von Neumann–Bernays–Gödel set theory
- Intuitionistic type theory
- Lambda cube
- Dependent type
- Dependent type
- Linear type system
- Axiom of constructibility
- System F
- Type theory
- Inductive type
- Gödel's consistency of CH and AC
- Jensen's covering theorem
- System F
- Calculus of constructions
- Calculus of inductive constructions
- Von Neumann–Bernays–Gödel set theory
- Strong normalization of simply typed lambda calculus
- Class
- Inner model
- Naive set theory
- Class
Further reading
About this page
| Tag | 4CVPENYR0S |
|---|---|
| URI | m2://4CVPENYR0S |
| Kind | proof |
| Writing | W0 stub |
| MSC | 03E30 |
| Proves | Russell's paradox |
| Uses | Set, Element |
| Methods | Proof by contradiction |
| Changed | 4 November 2026 |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- an inventory row: the row of the inventory that the node accounts for (0 of 1)
- a source with a locator (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.
What links here
No page links to this page yet.