How Types avoids Russel's Paradox?

Question

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

Answer 1

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.

Answer 2

Here's a rough loose-goosey explanation.

---

For any type t we have a type denoted set(t), along with an operation _∈_ : t → set(t) → 𝔹, where 𝔹 are the booleans.

Now the type of ∈ is already sufficient to dismiss Russell's paradox ─more or less.

This is because we cannot form the expression X ∈ X as it is ill-defined and so Russell's set {x : set | x ∉ x } is ill-typed since ∈ is not between sets at the same level, moreover, set needs to be over some type.

Answer 3

In MLT or CIC type thery (and HoTT), they use a hierarchy of universes, it is quite similar to the Grothendieck universe construction in the Tarski–Grothendieck set theory, which asserts for each set, there is some universe set containing it, a universe set is a model of ZFC, so every basic construction operation can be carry out within that universe, but not these operations applied on the universe. This is how TG set theory avoids Russell paradox. In TT, a similar construction is presented, namely $U_1:U_2:U_3:\cdots$, so it avoids Russell paradox by throwing propositions about one level to a next level. Actually, any directed set suffices to serve as indices. The existence of universe is basically asserting the existence of inaccessible cardinals, which essentially saying you cannot construct that level using basic set theoretical operations (or in TT, basic type constructions) like union, powerset, replacement, etc.

I think TT and ST are quite the same in expressive power, but ST uses FOL as its logic, and TT's logic is itself, and it is intuitionistic in nature.