module 1Lab.Counterexamples.Russell where

Russell’s paradox🔗

This page reproduces Russell’s paradox from naïve set theory using an inductive type of Type-indexed trees. By default, Agda places the type Type₀ in Type₁, meaning the definition of V below would not be accepted. Since we’re defining a data type, Agda allows us to attach the NO_UNIVERSE_CHECK pragma, which disables this checking for the definition of V.

{-# NO_UNIVERSE_CHECK #-}
data V : Type where
  set : (A : Type)  (A  V)  V

The names V and set are meant to evoke the cumulative hierarchy of sets. A ZF set is merely a particular type of tree, so we can represent the cumulative hierarchy as a particular type of trees - one where the branching factor of a node is given by a type A.

We define the membership predicate _∈_ by pattern matching, using the path type __:

_∈_ : V  V  Type
x  set A f = Σ A λ i  f i  x

A set x is an element of some other set if there exists an element of the index type which the indexing function maps to x. As an example, we have the empty set:

Ø : V
Ø = set  λ ()

X∉Ø : {X : V}  ¬ X  Ø
X∉Ø ()

Given the _∈_ predicate, and the fact that we can quantify over all of V and still stay in Type₀, we can make the set of all sets that do not contain themselves:

R : V
R = set (Σ _ λ x  ¬ x  x) fst

If X is an element of R, then it does not contain itself:

X∈R→X∉X : {X : V}  X  R  ¬ X  X
X∈R→X∉X ((I , I∉I) , prf) elem =
  let I∈I : I  I
      I∈I = subst  x  x  x) (sym prf) elem
  in I∉I I∈I

Using a diagonal argument, we can show that R does not contain itself:

R∉R : ¬ R  R
R∉R R∈R = X∈R→X∉X R∈R R∈R

And every set that doesn’t contain itself is an element of R:

X∉X→X∈R : {X : V}  ¬ X  X  X  R
X∉X→X∈R X∉X = (_ , X∉X) , refl

This leads to a contradiction.

Russell : 
Russell = R∉R (X∉X→X∈R R∉R)