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
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
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
b are different by the above
Different to define
NonExistent, such that for
o : Ω and
r : ℝ,
NonExistent o r is populated iff all values taken by
r, by the above definition of “different”. Note the
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
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 .