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

module Cantor where

open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

Then we define negation, as usual, using ,

data: Set where

¬ :  {}  Set Set ℓ
¬ p = p 

and introduce a Bit type

data Bit : Set where
  Z : Bit -- "Zero"
  O : Bit -- "One'

and a simple utility function

flip : Bit  Bit
flip Z = O
flip O = Z

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 .

 : Set= Bit

I was actually stuck for a while doing this proof because I tried modeling 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 , 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 ,

Ω : Set
Ω =

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.

data Different (a b :) : Set where
  different : (n :)  ¬ (a n ≡ b n)  Different a b

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!

data NonExistent (order : Ω)  (r :) : Set where
  non-existent : ((n :)  Different (order n) r) 
                   NonExistent order r

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 :

construct : Ω  ℝ
construct f = λ n  flip (f n n)

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:

flip-lemma : (x : Bit)  ¬ (x ≡ flip x)
flip-lemma Z ()
flip-lemma O ()

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 .

cantor : (o : Ω)  Σ ℝ (λ r  NonExistent o r)

The we produce is given by construct o, and the proof by a simple variation on flip-lemma that tells us that .

cantor o = construct o , non-existent (
             λ n  different n (flip-lemma (o n n)))