**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)^{5}:

*
¬
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^{n}) mod 10)/(10^{n})

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