Are real numbers countable in constructive mathematics?

Question

We are talking about ordinary reals in constructive mathematics.

1. Let represent each real number by infinite converging series: $$r = [\;(a_0,b_0),(a_1,b_1),...,(a_i,b_i),...\;]$$ $$where\quad a_i \leq b_i\quad and \quad a_i \leq a_{i+1} \; and \; b_{i+1} \leq b_i$$

   And interval $(a_i,b_i)$ converges: for any given rational $e > 0$ there is index $j$ such that $b_k - a_k < e$ for all $k \geq j$.

2. There are only one way to construct such a number: to build an algorithm that produces $ (a_{i+1},b_{i+1}) $ from (a,b) (or some nearly equivalent).

3. Let model algorithms by lambda terms (we are able to do so because lambda calculus is Turing complete).

4. It is easy to show that each lambda term may be represented by unique natural number (this is simple serialization/deserialization process, well known for every programmer).

5. So there is a one-to-one correspondence between real numbers and subset of natural numbers.

6. This imply that constructive reals and naturals are equipotent sets.

What are not ok with this reasoning and why?

Answer 1

I am going to attempt another answer which directly addresses what you wrote.

It cannot be shown constructively that every infinite subset of $\mathbb{N}$ is in bijective correspondence with $\mathbb{N}$. Thus your reasoning has a flaw when going from step 4 to step 5. By "infinite set" here I mean that there is an injective sequence from $\mathbb{N}$ into the set. "Bijective correspondence" means there is a bijection and its inverse between the sets. Concretely:

Theorem: Suppose every infinite subset of $\mathbb{N}$ is in bijective correspondence with $\mathbb{N}$. Then we can solve the Halting problem (assuming Markov principle).

Proof. The set $$S = \lbrace n \mid \text{the $n$-th Turing machine diverges}\rbrace$$ is obviously infinite. Suppose we had a surjection $b : \mathbb{N} \to S$. But then we can semidecide whether a given Turing machine diverges, so we can decide whether a given Turing machien halts. (There is a hidden use of Markov principle here, can someone get rid of it?) QED.

Likewise, in your concrete example, it cannot be shown constructively that there is a bijection between $\mathbb{N}$ and constructive reals, or lambda terms representing them, even though it is the case that the lambda terms representing reals are in bijective correspondence with a subset of $\mathbb{N}$. That was precisely the point of my first answer: I gave a proof that any attempt at enumeration of the reals omits a real.

Furthermore, from discussion in my other answer it seems that you claim that in constructive mathematics all subsets of $\mathbb{N}$ are constructively enumerable. That is false. The set $S$ from the above proof is an example of a set which cannot be constructively enumerated. The set $S$ is of course constructively well defined (or "built" in your sense), as it is not too hard to write down a formula that describes it (using Kleene's predicate $T$).

Answer 2

It depends on what you mean.

If you are working in classical mathematics, and regard the computable reals to be those real numbers for which a program exists to generate their digits, then they are countable, since there are at most (classically) countably many programs.

However, if you are working in intuitionistic mathematics, then after you construct the real numbers you can prove using a standard diagonalization argument that the reals are not countable. This shows that the real numbers are not constructively countable. There is no computable construction which puts the computable reals into bijective correspondence with the natural numbers, since that would require the ability to solve the Halting problem -- ie, how do you tell if two programs generate the same stream of digits?

Answer 3

I gave Neel's ansswer +1 and just for reference, here is a constructive proof showing that the real numbers are not countable.

Let $x_1, x_2, x_3, \ldots$ be a sequence of real numbers. We seek a real number which is different from all terms of the sequence. We first define by recursion a sequence of nested intervals $[a_i, b_i]$ with rational endpoints such that the width of the $n$-th interval is $(2/3)^n$. Let $[a_0, b_0] = [0,1]$. Suppose $[a_n, b_n]$ has been constructed. Let $c = (2 a_n + b_n)/3$ and $d = (a_n + 2 b_n) / 3$. Then $c < x_n$ or $x_n < d$. Define

$[a_{n+1}, b_{n+1}] = [a_n, c]$ if $c < x_n$

$[a_{n+1}, b_{n+1}] = [d, b_n]$ if $x_n < d$

where it does not matter which of the two cases we choose when both $c < x_n$ and $x_n < d$. (This is ok and it amounts to constructively acceptable Countable choice.)

Let $y = \lim_{n \to \infty} (a_n + b_n)/2$. The limit exists because the midpoints of the intervals form a Cauchy sequence whose rate of convergence is $(2/3)^n$. The real number $y$ is distinct from $x_n$ because $y \in [a_n, b_n]$ but $x_n \not\in [a_n, b_n]$ by construction.

A comment: your "definition" of reals as sequences of nested intervals is fishy because you do not talk about and conditions that require the widths of the intervals to converge to $0$. Also, please note that the set of those $\lambda$-terms which represent sequences of nested intervals with rational endpoints and whose witdhs converge to 0 is not recursively enumerable.

Answer 4

You are using the word "constructive" in an unusual way. It is true that, in ZFC, the set of computable real numbers is countable, but that is not directly a statement about constructive mathematics.

Not every school of constructive mathematics identifies real numbers with algorithms; that's a characteristic of the "Russian" school as I understand it. In other schools of constructivism that I am more familiar with, real numbers are coded by elements of $2^\omega$, or by a certain type of Dedekind cut on the rationals. In such schools it is not universally assumed that every real number is associated with a finite algorithm.

Even in the Russian school, they would not say that the set of real numbers is countable. Because, if you identify real numbers with algorithms, there is no computable enumeration of computable reals that lists all computable reals, and so the translation of "the real numbers are countable" into this setting is false.

That phenomenon also occurs in classical computable analysis. The subsystem RCA₀ of second-order arithmetic has a model in which every real number is computable. But this subsystem still proves that there is no surjection $\mathbb{N}\to\mathbb{R}$.

Answer 5

Let me interpret your constructive terminology to mean definable with respect to some countable first order language, since although this may not be your original focus, there is something interesting to say about it.

One often hears it said that there must be reals that we cannot define or describe, because there are only countably many definitions, but uncountably many reals. And if one considers only definitions over a fixed first-order structure in a countable language, then this is correct for the reason you describe. Nevertheless, there is another very curious sense in which it can fail, which I would like to explain.

An object $w$ in a first-order structure $M$ is definable (without parameters) if there is a formula $\varphi(x)$ such that $w$ is the only object in $M$ satisfying $\varphi(w)$.

For example, there are no definable reals at all in the structure of the reals $\langle\mathbb{R},\lt\rangle$ as a pure order, because any two elements are automorphic. In the ordered real field $\langle\mathbb{R},+,\cdot,\lt,0,1\rangle$, we lose these automorphisms and gain many definable reals, but only countably many, because there are only countably many definitions. More reals become definable with additional structure $\langle\mathbb{R},+,\cdot,\lt,0,1,exp,sin,\ldots,\rangle$, but in a countable language, there are still only countably many definable reals.

We can also extend the structure to higher orders, such as second-order analysis or higher levels of the set-theoretic hierarchy. For example, for a given infinite ordinal $\theta$, one could look at the definable reals that exist in the set-theoretic universe $\langle V_\theta,{\in}\rangle$, which even for moderate $\theta$, such as $\theta\gt\omega^2$, would include all of the usual classical structure on the reals, as these are definable in a comparatively small amount of set theory. But still, since this language is countable, there would still be only countably many definable reals.

Suppose we should go all the way? Let's consider the reals that might be defined within set theory at all, without cutting off the universe at $\theta$.

Question. Can there be a model $W$ of ZFC which thinks of each of its reals that it is definable without parameters?

The curious answer is Yes! And this is the sense I mentioned at the begining in which the original inquiry can fail.

This property is already exhibited by what is known as the minimal model of ZFC, the smallest $L_\alpha\models ZFC$. Similar models can be built by taking definable Skolem hulls inside any model with a definable Skolem function. More generally, Jonas Reitz, David Linetsky and I, building on results of Ali Enayat and Steve Simpson, have proved:

Theorem. Every countable model $W$ of ZFC has a class forcing extension $W[G]$, a model of ZFC, in which every object is definable without parameters.

Thus, in the model $V=W[G]$, every object whatsoever happens to be definable without parameters. In particular, in this universe it happens that every particular real is definable without parameters, even though the language is countable.

The resolution of the resulting paradox is that the property of "being definable" is not first-order expressible. Although the model thinks that there are uncountably many reals, each of which happens to uniquely fulfill a definition, and it thinks that there are only countably many definitions, it is nevertheless unable to map those definitions onto the reals, since by Tarski's theorem, there is no universal truth definition. So it is unable to build the countable sequence of definable reals against which we might diagonalize to produce a non-definable real.

Answer 6

I'd like to emphasise a few relevant distinctions. First, as mentioned, is the various senses of "constructive". The important two here are Markov's (russian) tradition, where it is assumed that all functions are computable. The other is Bishop's tradition, where all assumptions are valid both classically and in Markov's tradition (and in other senses). So, Bishop's school does not assume that there are non-computable functions, but neither does it assume that all functions are computable.

Andrej's earlier proof is in Bishop's tradition. There are of course proofs that the computable real numbers are not computably enumerable, and other proofs that the classical real numbers are not classically enumerable. But the proof he posted is a unifying proof that the real numbers are not enumerable.

A second distinction is between the set of real numbers and the set of infinite binary sequences. A bijection exists classically, but is non-constructive. A third distinction is between these two sets, and the class of all subsets of $\mathbb{N}$. It is useful to talk about sets of natural numbers, even if their characteristic function is undecidable. For instance, the set of (codes for) lambda terms of convergent series (Cauchy sequences). This is a subset of $\mathbb{N}$, but only classically does its characteristic function exist, so only classically will it be an element of the set $2^\mathbb{N}$.

Finally, there is the distinction between countable and subcountable. A set is subcountable if it is the image of a subset of $\mathbb{N}$. Classically, every subcountable set is countable, but not so constructively. There are even simple models of CZF (a version of ZF with intuitionistic logic) where every set is subcountable (even within the model), whereas the set of real numbers, as said above, is not countable.

So, with all these in mind:

The real numbers are not countable. But there is proof, in Markov's tradition, that the real numbers are subcountable - which is basically yours, since the set of valid lambda terms is a subset of $\mathbb{N}$.

There is a diagonal argument, valid in Bishop's tradition, that $2^\mathbb{N}$ is not countable, but similarly there is a Markovian proof that $2^\mathbb{N}$ is subcountable. Finally, there is a diagonal argument, valid in Bishop's tradition, that the class of all subsets of $\mathbb{N}$ is not even subcountable.

Answer 7

Incorrect.

The problem is that intuition breaks down when dealing with infinities. There are more real numbers than there are integers. The unfortunate part, from a computer scientist's standpoint, is that I will never be able to present you with a satisfying counter-example, except perhaps for Chaitin's number - http://en.wikipedia.org/wiki/Chaitin's_constant . The problem comes about (essentially) because many numbers (indeed, almost all numbers) have a decimal representation of infinite length, but your programs must be of finite length. So there's a bad assumption here - you are assuming that all real numbers can be defined by a finite program in the lambda calculus, and that is an untrue statement. If you allow infinite programs (although I don't really see how one could do that rigorously, but heck, let's continue this thought experiment) then your statement could be correct, but trading infinite decimal representations for infinite programs is probably not a net win.

Basically, there are so many more real numbers than there are integers that intuition is almost entirely unsuitable for reasoning in this domain. To see counter-examples in this from computer science, consider the classic diagonalization proofs for uncomputability. This result is usually shown to prove that there exist languages which no Turing machine can compute, but it also shows that the number of languages (the number of "problems") is strictly greater than the number of programs (the number of "solutions"). Indeed, it shows that the number of languages is equal to the number of real numbers, and the number of programs is equal to the number of integers!

Even worse, there are only countably many mathematical constructions, computer programs, and English essays, so if you try and get around the "lambda calculus" or "turing machine" part with vigorous handwaving, you still end up in a situation where you have fewer descriptions available to you than you have numbers to describe. Unfortunately, for obvious reasons, I can't describe any of these indescribable numbers to you.

More about this can be found in texts on computational complexity, or the theory of computation, or, more directly but also less-accessibly, texts on Kolmogorov complexity.