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. The
--type-in-type
flag disables this check, meaning the
definition goes through.
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 ⊥ absurd 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)