NFE Home 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