Cantor’s diagonal argument, in principle, proves that there can be no bijection between $\mathbb{N}$ and $\{0, 1\}^\omega$ ($\omega$ here is countable infinity, the cardinality of $\mathbb{N}$). Depending on what logic you operate in (classical versus constructive) this has implications on the relative cardinality of $\mathbb{N}$ and $\mathbb{R}$ (“is $\mathbb{R}$ bigger, in some sense of the word, than $\mathbb{N}$?”). The proof itself is constructive, and can be modeled within a theorem prover like Agda (or Coq) without artificially introducing LEM. This post is about modeling it in Agda.

First, some bookkeeping

Then we define negation, as usual, using $\bot$,

and introduce a Bit type

and a simple utility function

One way to model $\{0, 1\}^\omega$ (denoted here as $\mathbb{R}$ for fun, but we haven’t proven any relation of that set with the set of real numbers) is as a function from $\mathbb{N}$ to $\{0, 1\}$.

I was actually stuck for a while doing this proof because I tried modeling $\{0, 1\}^\omega$ as a coinductive list of Bits. Turns out working with function application is much easier.

Cantor’s argument is proof by contradiction: it proceeds by showing that given a mapping $f : \mathbb{N} \mapsto \{0, 1\}^\omega$ , there is an $r \in \{0, 1\}^\omega$ such that $\forall n \cdot f(n) \neq r$. This implies that $f$ cannot also be a surjective function, and hence isn’t a bijection.

In Agda, we model $f$ as a value of type $\Omega$,

and inequality between $a, b \in \{0, 1\}^\omega$ as $\exists n \cdot a \downarrow n \neq b \downarrow n$ where $x \downarrow y$ means “the $y^{th}$ digit of $x$”. In Agda, we create a data-type Different such that Different a b is populated (i.e. there is a value of that type) iff a and b are different by the above criterion.

We use Different to define NonExistent, such that for o : Ω and r : ℝ, NonExistent o r is populated iff all values taken by o is different from r, by the above definition of “different”. Note the bracketing in non-existent (as opposed to different) – it makes all the difference in the world!

Cantor’s trick was, given a mapping $f : \mathbb{N} \mapsto \{0, 1\}$, to create a value $v \in \{0, 1\}$ such that it was different from all values taken by $f$ at at least one “digit”. Specifically, the $n^{th}$ digit of $v$ would be the inverse of the $n^{th}$ digit of $n^{th}$ value produced by $f$:

Once set up this way, the proof itself is surprisingly simple – we just need one additional simple lemma stating that flip x is never equal to x:

The proof asserts (using the dependent product type Σ defined in Data.Product to model $\exists$) that given a mapping $o : \mathbb{N} \mapsto \{0, 1\}^\omega$, we can find $r$ such that everything $o$ produces is different from $r$.

The $r$ we produce is given by construct o, and the proof by a simple variation on flip-lemma that tells us that $\forall n \cdot o(n) \downarrow n \neq r \downarrow n$.