[FOM] Constructivism, Geometry, and Powerset

[Andrej Bauer]

Dear Arnon,

> 4) From 2 and 3 it follows that Andrej cannot prove that
>   his R^2 is uncountable.

You are mistaken. I already said that every constructive school shows
R to be uncountable. In face of your denial of these facts, I present
below a constructive proof that R is uncountable, without the use of
powersets.

Let R be the construction I outlined in my post from Sat May 16
02:44:53 EDT 2009,
http://www.cs.nyu.edu/pipermail/fom/2009-May/013632.html , i.e., the
quotient of Cauchy sequences of rational numbers. In this post we
additionally assume dependent choice (to make the proofs somewhat more
intuitive, although countable choice would suffice). In that post I
also commented on the relationship between exponentials, powersets,
and classical logic, which Arnon might want to read again since it
contains an explanation of where he is making a mistake.

We prove intuitionistically that R is uncountable in the following
sense: for every sequence in R there is a real number which is
different from all terms of the sequence (it is even at a positive
distance from every term). We use the fact that R is a Cauchy-complete
ordered field.

First observe that given an interval [a,b] (which is represented as a
pair of numbers a,b such that a < b) and a real number x, there is an
interval [c,d] such that:
(i) x is not a member of [c,d], i.e, x < c or x > d.
(ii) the width of [c,d] is at most half of the width of [a,b], i.e., 2
(d - c) <= b - a.
(iii) [c,d] is contained in [a,b], i.e., a <= c < d <= b.
Specifically, either x < (a + 2 b)/3 or x > (2 a + b)/3. In the first
case take [c,d] = [a,(3a+b)/4], and in the second [c,d] = [(a+3b)/4,
b].

Let x : N -> R be any sequence of real numbers. We define a sequence
of nested intervals [a_n, b_n] as follows. Let [a_0, b_0] = [0, 1].
Suppose [a_n, b_n] has been constructed. Using dependent choice we may
choose [a_{n+1}, b_{n+1}] satisfying the above properties (i)-(iii)
with respect to [a_n, b_n] and x_n. This gives us a sequence of nested
intervals [a_n, b_n] such that the midpoints q_n = (a_n+b_n)/2 form a
Cauchy sequence whose limit y = lim_n q_n is different from every term
x_n. This is so because y is contained in [a_n, b_n] but x_{n+1} is
not, hence |x - y| >= 2^{-n-1}. Therefore R is uncountable.

The above proof as well as the construction of R are valid in
classical logic. And one more thing. Please stop calling me
"constructivist" because I am not. The difference between us is not in
our beliefs but in our understanding of constructive mathematics.

With kind regards,

Andrej