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 = rThe standard proof uses Cantor's diagonal method and proceeds as follows: Let a be any sequence of real numbers. Define a sequence b by
bn := (9 - trunc(an * 10n) mod 10)/(10n)In CASL, this can be defined by
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.
b = ConstSeq(9) - trunc(a*ConstSeq(1::0) ^ N) mod ConstSeq(1::0)