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:

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)

{-#  OPTIONS --type-in-type #-}

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)