# 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

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. – Musa Al-hassy Aug 11 '16 at 18:28
• @MusaAl-hassy The universe in NF contains all sets, not just sets of some specified level. – Martin Berger Aug 11 '16 at 22:48
• So $U$ contains itself, but there's no way to say this because $U\in U$ is not a valid formula? – celtschk Aug 13 '16 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. – Martin Berger Aug 13 '16 at 13:31

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 constrcution 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 Russlel 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 ;) – Musa Al-hassy Aug 12 '16 at 16:33