I gone through the Russel's paradox. From Wikipedia :According to naive set theory, any definable collection is a set. Let R be the set of all sets that are not members of themselves. If R is not a member of itself, then its definition dictates that it must contain itself, and if it contains itself, then it contradicts its own definition as the set of all sets that are not members of themselves. Next Russell's and Alonzo Church developed type theory to avoid this paradox. Can someone explain clearly how these types (type theory) avoids this paradox. Thanks
How Types avoids Russel's Paradox?
type theory;mathematical foundations
There is a second solution to the conundrum, which is Quine's NF (New Foundations) set theory.NF is a set theory that avoid the paradox, but a set of all sets does exist. NF avoids Russell's paradox by putting constraints on the what formulae are allowed in comprehension. In other words the predicate $\phi$ in$$   \{x\ |\ \phi(x)\}$$does not range over all predicates, but only over predicates that are well-stratified. In particular, $true$ is well-stratified, so the universe$$   U = \{x\ |\ true\}$$is a set in NF. A first-order logic formula $\phi$ in the language of set-theory (i.e. $\in$ is the sole non-equality predicate) is well-stratified, provided there is a function $$level : Vars \rightarrow \mathbb{N}$$(Here $Vars$ is the set of all variables) such that the following holds.For all sub-formulae $x \in y$ in $\phi$: $level(x) + 1 = level(y)$.For all sub-formulae $x = y$ in $\phi$: $level(x)  = level(y)$.In summary, while ZF(C) set-theory avoids Russell's paradox by prohibiting sets that are too big, NF avoids Russell's paradox by prohibiting sets that are too ugly.