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)