New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ru GIF version

Theorem ru 2468
 Description: Russell's Paradox. Proposition 4.14 of [TakeutiZaring] p. 14. In the late 1800s, Frege's Axiom of (unrestricted) Comprehension, expressed in our notation as A ∈ V, asserted that any collection of sets A is a set i.e. belongs to the universe V of all sets. In particular, by substituting {x ∣ x ∉ x} (the "Russell class") for A, it asserted {x ∣ x ∉ x} ∈ V, meaning that the "collection of all sets which are not members of themselves" is a set. However, here we prove {x ∣ x ∉ x} ∉ V. This contradiction was discovered by Russell in 1901 (published in 1903), invalidating the Comprehension Axiom and leading to the collapse of Frege's system. Russell developed a system that avoids the paradox with his "theory of types." Quine extended Russell's ideas to formulate his New Foundations set theory, which we formalize below. Thus in a very real sense Russell's Paradox spawned the invention of NF set theory and completely revised the foundations of mathematics!
Assertion
Ref Expression
ru {x x x} V

Proof of Theorem ru
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 pm5.19 346 . . . . . 6 ¬ (y y ↔ ¬ y y)
2 eleq1 1954 . . . . . . . 8 (x = y → (x yy y))
3 df-nel 2015 . . . . . . . . 9 (x x ↔ ¬ x x)
4 id 18 . . . . . . . . . . 11 (x = yx = y)
54, 4eleq12d 1962 . . . . . . . . . 10 (x = y → (x xy y))
65notbid 282 . . . . . . . . 9 (x = y → (¬ x x ↔ ¬ y y))
73, 6syl5bb 245 . . . . . . . 8 (x = y → (x x ↔ ¬ y y))
82, 7bibi12d 309 . . . . . . 7 (x = y → ((x yx x) ↔ (y y ↔ ¬ y y)))
98a4v 1671 . . . . . 6 (x(x yx x) → (y y ↔ ¬ y y))
101, 9mto 164 . . . . 5 ¬ x(x yx x)
11 abeq2 1994 . . . . 5 (y = {x x x} ↔ x(x yx x))
1210, 11mtbir 287 . . . 4 ¬ y = {x x x}
1312nex 1366 . . 3 ¬ y y = {x x x}
14 isset 2304 . . 3 ({x x x} V ↔ y y = {x x x})
1513, 14mtbir 287 . 2 ¬ {x x x} V
16 df-nel 2015 . 2 ({x x x} V ↔ ¬ {x x x} V)
1715, 16mpbir 197 1 {x x x} V
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ↔ wb 173  ∀wal 1322  ∃wex 1327   = wceq 1398   ∈ wcel 1400  {cab 1882   ∉ wnel 2013  Vcvv 2300 This theorem is referenced by:  epprc  5046 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1323  ax-6 1324  ax-7 1325  ax-gen 1326  ax-8 1402  ax-10 1403  ax-11 1404  ax-12 1405  ax-17 1413  ax-9 1424  ax-4 1429  ax-16 1606  ax-ext 1877 This theorem depends on definitions:  df-bi 174  df-an 357  df-ex 1328  df-sb 1568  df-clab 1883  df-cleq 1888  df-clel 1891  df-nel 2015  df-v 2302
 Copyright terms: Public domain W3C validator