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$$.

$\Box$