 Despite Quine’s comment, it is possible to see Russell’s paradox in a more positive light. For one thing, although the matter remains controversial, later research has revealed that the paradox does not necessarily short circuit Frege’s derivation of arithmetic from logic alone. Frege’s version of NC (his Axiom V) can simply be abandoned. (For details, see the entry on  Frege’s Theorem.)  For another, Church gives an elegant formulation of the simple theory of types that has proven fruitful even in areas removed from the foundations of mathematics. (For details, see the entry on  Type Theory.)  Finally, the development of axiomatic (as opposed to naïve) set theories which exhibit various ingenious and mathematically and philosophically significant ways of dealing with Russell’s paradox paved the way for stunning results in the metamathematics of set theory. These results have included  Gödel’s  and Cohen’s theorems on the independence of the  axiom of choice  and Cantor’s continuum hypothesis. So let us see, roughly, how some of these methods – specifically, the so-called “untyped” methods – deal with Russell’s paradox.