# How Types avoids Russel's Paradox?

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

• plato.stanford.edu/archives/spr2010/entries/type-theory Aug 5, 2016 at 5:55
• This phenomenon is all over the literature und the web. What have you read? Do you have a specific question? Reproducing textbook chapters is not a worthwhile use of anybody's time. Aug 5, 2016 at 7:49

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.

• Yes, this is a brillinat idea: using levels for each set to avoid issues. This allows us to say "the set of all sets of level i" and indeed such a set cannot belong to itself. This idea is in popular usage under the name of universes of dependent types, such as in the (Haskell-syntax-like) Agda language for example. Aug 11, 2016 at 18:28
• @MusaAl-hassy The universe in NF contains all sets, not just sets of some specified level. Aug 11, 2016 at 22:48
• So $U$ contains itself, but there's no way to say this because $U\in U$ is not a valid formula? Aug 13, 2016 at 13:06
• @celtschk Yes, and that leads to all manner of interesting questions like what's the powerset of $U$, can $U$ be well-ordered, are all ordinals comparable etc. Aug 13, 2016 at 13:31
• @celtschk No, that's not quite right. The formula $U \in U$ is a valid formula, and furthermore, it's true. For that matter, $x \not\in x$ is a valid predicate, and it's true for some values of $x$ and false for others. However, there is no set containing exactly those values of $x$ which satisfy this predicate. Apr 19, 2021 at 20:05

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.

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.

• I just want to point out that this seems to be the common idea to avoid the paradox, as you write, avoid Russell's paradox by throwing propositions about one level to a next level. This is what other theories essentially seem to do as well ;) Aug 12, 2016 at 16:33