M-7 -- 5.1 Proof of the Uncountability of the Reals

Go up to 5 More About the Specification BasicReal
Go forward to 5.2 The Categoricity of the Reals

5.1 Proof of the Uncountability of the Reals

The uncountability of the reals means that there is no function from the natural numbers to the real numbers (i.e. sequence of real numbers) that is surjective (i.e. every real number occurs in the sequence)⁵:

¬ exist a:Nat -> Real . forall r:Real . exist n:Nat . a ! n = r

The standard proof uses Cantor's diagonal method and proceeds as follows: Let a be any sequence of real numbers. Define a sequence b by

b_n := (9 - trunc(a_n * 10ⁿ) mod 10)/(10ⁿ)

In CASL, this can be defined by

b = ConstSeq(9) - trunc(a*ConstSeq(1::0) ^ N) mod ConstSeq(1::0)

Then it is easy to show that partialsum(b) is a Cauchy sequence. By Cauchy completeness, sum(b) is defined. Now the decimal representation of sum(b) differs from that of a<n> in the n-th digit after the comma. Thus, sum(b) is not in the range of a, and a is not surjective. That is, there cannot be a sequence mapping of the natural numbers onto the real numbers. Hence, the real numbers are uncountable.

CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.
Comments to till@informatik.uni-bremen.de