# Russell's Paradox - Agda Edition

*This short post contains some Agda code from a **Thorsten Altenkirch's lecture** on **Russell's paradox**. I've first heard of this lecture via **Liam O'Connor's blog** which has a broad exposition on the subject and informs a lot of the following. The "annotations" between code cells correspond to my attempt at understanding (universes of) types and I hope it can make Agda explorations easier for others: you can **remix** this article or **run it** to experiment with Agda's paradoxical type-in-type mode.*

Let's first state the paradox as follows: if we allow *unrestricted comprehension* (that is the specification of a collection of objects - a set - by means of a valid predicate) then we're allowed to construct the *set of all sets which don't belong to themselves*

This is a quite reasonable statement in a model of naïve set theory, but now we're also allowed to ask if inline_formula not implemented. If it does then by construction inline_formula not implemented. And conversely if inline_formula not implemented then actually inline_formula not implemented. This is pretty controversial!

Russell's alternative foundations for avoiding the paradox *Mathematical Logic as Based on the Theory of Types** *(1908), an ancestor of modern type theory, refutes the idea of a *set of all sets* and introduces the idea of a hierarchy of types to bypass self-referential issues:

*[...] we explained a doctrine of types of variables, proceeding upon the principle that any expression which refers to all of some type must, if it denotes anything, denote something of a higher type than that to all of which it refers. Where "all" of some type is referred to, there is an "apparent variable" belonging to that type. Thus any expression containing an apparent variable is of higher type than that variable. *

And but probably the deceiving point is to allow *set constructors* to use the very terms of the language - first order logic over the binary membership relation - and it costed set theorists piles of axioms to be sorted out and constrained to avoid inconsistencies. The problem is somehow avoided in type theory, where the *predicate* "x belongs to S" (inline_formula not implemented) is replaced by a *typing judgement*

requiring an *external* authority (a type checker) to decide that "the term x is of type T in some context inline_formula not implemented". In this setup it doesn't make sense to construct a type in terms of the typing judgement itself. Around this topic, I found the introduction of the HoTT book on type theory quite enlightening:

*...in set theory, “membership” is a relation which may or may not hold between two pre-existing objects “a” and “A”, while in type theory we cannot talk about an element “a” in isolation: every element by its very nature is an element of some type, and that type is (generally speaking) uniquely determined. Thus, when we say informally “let x be a natural number”, in set theory this is shorthand for “let x be a thing and assume that x ∈ N”, whereas in type theory “let x : N” is an atomic statement: we cannot introduce a variable without specifying its type.*

Let's now turn to some code: like in axiomatic set theory as ZFC and Russell's types, in order to avoid paradoxes of the above kind Agda relies on a strict hierarchy of types or universe levels:

formula not implemented`module Universes where`

`open import Level`

`open import Relation.Unary`

`ϕ : {l : Level} → Set (suc l)`

`ϕ {l} = Set l`

`-- like in Russell's words: "any expression containing an apparent variable is of higher type than that variable"`

`ψ : {l m : Level} → (A : Set l) → Set (l ⊔ suc m)`

`ψ {_} {m} A = A → Set m`

Now, we can tell Agda to collapse the hierarchy to just one level (level 0), by running the interpreter with the `--type-in-type`

option. (Note: we'll be using two distinct nextjournal runtimes to demonstrate the effect of the pragma. We start a new one below)

`module Russell where`

`open import Data.Bool using (Bool; true; false; if_then_else_)`

`open import Data.Unit`

`open import Data.Product`

`open import Data.Empty`

`open import Relation.Binary`

`open import Relation.Binary.PropositionalEquality`

with the pragma on top of the module, Agda runs in a paradoxical mode, i.e. from the fact inline_formula not implemented, we'll be able to encode Russell's paradox.

`_ : Set`

`_ = Set`

let's define a self-referential way for building sets with an inductive data type

`data M : Set where`

` m : (I : Set) → (f : I → M) → M`

the above can read as: to *construct* a set in inline_formula not implemented we start from a type of indices inline_formula not implemented and a function inline_formula not implemented which describes the set by its image on inline_formula not implemented. Here Altenkirch uses the letter M as per *Menge*, german for set. Since M is a valid type now it can be used itself as indices. Note that in this definition we already use set-in-set as Agda won't allow this in a "normal" type-hierarchic runtime*:*

`data M : Set where`

` m : (I : Set) → (f : I → M) → M`

this tells us that using indices inline_formula not implemented would require inline_formula not implemented to live one level above in the hierarchy (namely level 1). We can construct the first three stages of Von Neumann hierarchy

`-- the empty set: with indices in the empty type (bottom: ⊥)`

`∅ : M`

`∅ = m ⊥ ⊥-elim`

`-- the set containing the empty set: indices are the unit type`

`[∅] : M`

`[∅] = m ⊤ (λ _ → ∅)`

`-- the set containing the empty set and the set containing the empty set`

`[∅,[∅]] : M`

`[∅,[∅]] = m Bool (λ x → if x then ∅ else [∅])`

we define a binary relation for membership as follows

`_∈_ : M → M → Set`

`a ∈ (m I f) = ∃[ i ] (a ≡ f i)`

In other words, the type inline_formula not implemented is *inhabited* (or the proposition inline_formula not implemented holds) if there exists an index which is mapped onto the set a via f. The existential notation actually denotes the dependent product (Sigma) type of inline_formula not implemented by inline_formula not implemented.

We can do some checks, finding evidence that Von Neumann sets are inhabited:

`_ : ∅ ∈ [∅]`

`_ = ( tt , refl )`

`_ : ∅ ∈ [∅,[∅]]`

`_ = ( true , refl )`

`_ : [∅] ∈ [∅,[∅]]`

`_ = ( false , refl )`

along the same lines, we define the negated membership

`_∉_ : M → M → Set`

`x ∉ y = x ∈ y → ⊥`

that is when inline_formula not implemented is inhabited, so is inline_formula not implemented which is a contradiction. Let's check that the empty set behaves as such

`∅-isEmpty : ∀ {s : M} → s ∉ ∅ `

`∅-isEmpty = proj₁`

this is pretty: assume a pair inline_formula not implemented witnesses membership of inline_formula not implemented in ∅, then index inline_formula not implemented is an inhabitant of inline_formula not implemented. We can now define the set R after Russell's

`R : M`

`R = m (Σ M λ s → s ∉ s) proj₁`

We'll derive the paradox via a combination of the following three lemmas

`lemma1 : ∀ { X : M } → X ∈ R → X ∉ X`

`lemma1 ((s , s∉s) , p) = subst₂ _∉_ p' p' s∉s where p' = sym p`

in the cell above inline_formula not implemented is a proof of inline_formula not implemented, thus we can transport the term inline_formula not implemented to inline_formula not implemented via `subst₂`

. Now the converse is also straightforward

`lemma2 : ∀ {X} → X ∉ X → X ∈ R`

`lemma2 {X} X∉X = ((X , X∉X) , refl)`

`lemma3 : R ∉ R`

`lemma3 = λ ( R∈R : R ∈ R) → lemma1 R∈R R∈R `

now since lemma3 shows that inline_formula not implemented is inhabited, we can derive a contradiction (i.e. an inhabitant of the empty type).

`⚡️ : ⊥`

`⚡️ = lemma3 (lemma2 lemma3)`