# Cantor's Diagonal Argument in Agda

Cantor’s diagonal argument, in principle, proves that there can be no bijection between and ( here is countable infinity, the cardinality of ). Depending on what logic you operate in (classical versus constructive) this has implications on the relative cardinality of and (“is bigger, in some sense of the word, than ?”). 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 ,

and introduce a `Bit`

type

and a simple utility function

One way to model (denoted here as for fun, but we haven’t proven any relation of that set with the set of real numbers) is as a function from to .

I was actually stuck for a while doing this proof because I tried
modeling as a coinductive list of `Bit`

s. Turns
out working with function application is much easier.

Cantor’s argument is proof by contradiction: it proceeds by showing that given a mapping , there is an such that . This implies that cannot also be a surjective function, and hence isn’t a bijection.

In Agda, we model as a value of type ,

and inequality between as where
means “the digit of ”. 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 , to create a value such that it was different from all values taken by at at least one “digit”. Specifically, the digit of would be the inverse of the digit of value produced by :

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 ) that given a mapping , we can find such that
everything produces is different from .

The we produce is given by `construct o`

, and the proof by a
simple variation on `flip-lemma`

that tells us that .