# Are real numbers countable in constructive mathematics?

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?

-
any set whose elements can be described by finite length words in a (countable) alphabet is countable. This is just the statement that the existence of a surjective map $A\to B$ with $A$ countable implies that $B$ is countable. –  Mariano Suárez-Alvarez Jul 5 '10 at 18:05
It sounds like you're talking about the computable numbers, and yes, they are countable: en.wikipedia.org/wiki/Computable_number –  Rahul Jul 5 '10 at 18:07
"I've noticed one very interesting priminent trait of many MO attendants: when they see contradiction in some discourse (or that discourse contradicts their prior knowledge), they do not tend to scrutinize entire reasoning to find exact cause of contradiction: they simply ban entire discourse or arbitrary part of it." Evidence or quotation, please, for those of us not expert in these waters? –  Yemon Choi Jul 6 '10 at 7:56
@Yemon Choi: I'm not "expert in these waters" and note that I'm not talking about MOST but only about MANY people on MO. For example, Neel Krishnaswami (most upvoted answer) states below: 1. Reals are not countable because of diagonal argument 2. Computable reals are not countable because of Halting problem But said nothing about WHY my judgments flawed and WHERE the flaw is. –  Vag Jul 6 '10 at 8:47
@Vag: let me apologize for not being more explicit! The specific trouble with your argument is that there are multiple lambda terms which compute the same sequence, and so to form the reals we need to quotient by an equivalence relation on lambda terms. However, for two arbitrary programs, we can't decide whether two lambda terms compute the same sequence or not. But if we had a bijection between syntactic codes and reals, we could decide this -- we could take two reals, pick representatives, and use the bijection to see if they go to the same code or not. So no bijection exists. –  Neel Krishnaswami Jul 6 '10 at 9:45

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$).

-
You would'nt kill me for one more little question in comments? How we might to constructively define a subset of nats $A$ at all? Only by function from Nat to Bool. Right? Then, if we write simple program that picks zero, tests if it belongs to $A$, outputs it if yes, then picks successor if zero, tests and outputs and etc, then for any element $x$ our program will eventually picks $x$ and output it. Right? –  Vag Jul 6 '10 at 11:51
That's exactly the issue we're discussion above. In constructive set theory, a subset of $\omega$ is not at all the same as a function from $\omega$ to 2. –  Carl Mummert Jul 6 '10 at 12:26

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?

-

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.

-
I don't understand your first comment. As for your second, there are two notions of definability in first order logic: an individual object is definable if it is the unique satisfying instance of a definition; a subset of the domain is definable if it is the set of all satisfying solutions of a definition. There are of course many instances of infinite sets being definable, such as many intervals, rays, solution sets to certain equations, and so on. One can define reals as limits of definable sequences, but there are still only countably many definable sequences in any countable language. –  Joel David Hamkins Jul 6 '10 at 10:56
I'll try to restate first comment: Suppose we are working in theory T which is formed as constructive part of HOL with extended by axioms of ordered real field R. We have countably many statements of T that define reals. But we can not infer in T that R is countable. –  Vag Jul 6 '10 at 11:13
I agree. The point of my answer is that first, if we are using a fixed first order set structure in a countable language, then there will be reals that we cannot define in that structure. Second, we cannot generalize this to conclude abstractly that there are necessarily reals that we cannot define in set theory at all, because there are models of ZFC in which every real is definable, and for all we know, we live inside such a universe. The resolution of the paradox is that the notion of being definable is not first-order expressible inside the structure. –  Joel David Hamkins Jul 6 '10 at 16:37
"we live inside such a universe" As far as I know, amount of mass+energy in our universe (multiverse?) is finite and there exist minimal possible quant of mass/energy (see Bremmermann Limit). This implies that our universe is finite in any sense. –  Vag Jul 6 '10 at 20:09
I was referring to the mathematical universe (of sets), not the physical universe. –  Joel David Hamkins Jul 6 '10 at 20:28

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.

-
+1. This is a fine proof in Bishop's system. Do you know how the proof goes in CZF without countable choice? I assume the uncountability of the Dedekind reals is provable there, but I'm not very familiar with the system. –  Carl Mummert Jul 5 '10 at 23:16
Thanks! Convergence fixed. It was not "fushy" but mountain sized flaw. –  Vag Jul 6 '10 at 6:28
@Carl: I have wondered about it myself on several occasions. I do not know a proof of uncountability of Dedekind reals which avoids choice. I asked around and never got an answer so as far as I am concerned, this is an open question. –  Andrej Bauer Jul 6 '10 at 6:31
@Vag: seeing your most recent comment, now I am sure you should simply read Andrej's comments as proving what you agree with, namely that certain sets of lambda terms don't exist. In many branches of constructive mathematics, they are very willing to have sets that do not have characteristic functions, while if you think of sets as a data type "Set" then you are really thinking about characteristic functions, not sets. In your original proof, the "set" of lambda terms that encode real numbers is another set you cannot prove to exist, because there is no effective decision procedure for it. –  Carl Mummert Jul 6 '10 at 12:10
@Vag: You can define a set of lambda terms which denote real numbers (this set is not r.e.). Then you can define a map $f$ from this set to the reals, i.e., a functional relation (I think you would call this left unique right total, or the other way around, I am not sure). You cannot define a map going from reals to lambda terms constructively. You cannot show thow that $f$ is surjective, and you cannot show that $f$ is not surjective. You need additional assumptions to conclude anything specific about $f$. –  Andrej Bauer Jul 6 '10 at 12:57

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 RCA0 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}$.

-
Bishop's constructive mathematics has the property that if you prove something, then you can algorithmically extract a constructive witness to it. To slightly oversimplify, the witness to a real number will be a program generating a converging sequence of intervals (pairs of rationals). I'd call that algorithmic. –  Charles Stewart Jul 6 '10 at 8:12
@Charles Stewart. It's possible for an element $x$ of $2^\omega$ to code a real number in a particular model without there being any term for $x$. In that case, proof-theoretic methods won't help. Moreover, if the model is the standard model and $x$ really is uncomputable, no correct proof-theoretic method can extract an algorithm for $x$. A formalization of Bishop's system is satisfied by the standard model of arithmetic in all finite types. –  Carl Mummert Jul 6 '10 at 11:25

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.

-

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.

-
I wonder who you are talking about when you say that their "intuition breaks down" and that their "intuition is almost entirely unsuitable for reasoning in this domain". –  Dan Piponi Jul 6 '10 at 16:08
I suppose I am talking to the computer scientists I have known who have strayed from the constructive countable mathematics of most CS courses into the domain of the reals without ever having taken a real analysis course. The original question struck me as being very similar to others that I have fielded (as a half math/half CS undergrad) from people in that category. –  Peter Boothe Jul 7 '10 at 2:04
My motivation while asking was: "I want to know ALL about this interesting chain of reasoning" but not "My intuition stalemates me, help!". –  Vag Jul 7 '10 at 7:30
For intuition breaking point of view I've found interesting this conjunction: "Every real is approximable by unbounded computation, i.e. `may be written down', but it is unable to write down all reals." –  Vag Jul 11 '10 at 14:40
@Vag: I would point back to the countable/subcountable distinction. The real numbers are not countable, but they are subcountable from a certain constructive point of view, as I said in my answer. That means there is a partial surjection F from the integers to the reals. So in a sense we can write them all down: for every real x there is an integer n such that F(n)=x. Of course there is no procedure to decide for a given n whether F(n) is defined. –  Daniel Mehkeri Jul 11 '10 at 18:07