New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ru Unicode 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 , asserted that any collection of sets is a set i.e. belongs to the universe of all sets. In particular, by substituting (the "Russell class") for , it asserted , meaning that the "collection of all sets which are not members of themselves" is a set. However, here we prove . 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

Proof of Theorem ru
StepHypRef Expression
1 pm5.19 346 . . . . . 6
2 eleq1 1954 . . . . . . . 8
3 df-nel 2015 . . . . . . . . 9
4 id 18 . . . . . . . . . . 11
54, 4eleq12d 1962 . . . . . . . . . 10
65notbid 282 . . . . . . . . 9
73, 6syl5bb 245 . . . . . . . 8
82, 7bibi12d 309 . . . . . . 7
98a4v 1671 . . . . . 6
101, 9mto 164 . . . . 5
11 abeq2 1994 . . . . 5
1210, 11mtbir 287 . . . 4
1312nex 1366 . . 3
14 isset 2304 . . 3
1513, 14mtbir 287 . 2
16 df-nel 2015 . 2
1715, 16mpbir 197 1
 Colors of variables: wff set class Syntax hints:   wn 3   wb 173  wal 1322  wex 1327   wceq 1398   wcel 1400  cab 1882   wnel 2013  cvv 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