Return to 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?

Distilled answer:

1. Constructed reals are ok
2. All judgments are perfectly correct except (3)
3. Statement (3) is incorrect because while it is completely ok to talk about algorithms behind each real there is no way to prove that relation between series and corresponding lambda terms is left total and right unique, and no way to build a computable injective function from reals to lambda terms.

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?

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?

Distilled answer:

1. Constructed reals are ok
2. All judgments are perfectly correct except (3)
3. Statement (3) is incorrect because while it is completely ok to talk about algorithms behind each real there is no way to prove that relation from series to corresponding lambda terms left total and right unique, and no way to build a computable injective function from reals to lambda terms.

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?

Distilled answer:

1. Constructed reals are ok
2. All judgments are perfectly correct except (3)
3. Statement (3) is incorrect because while it is completely ok to talk about algorithms behind each real there is no way to prove that relation between series and corresponding lambda terms is left total and right unique, and no way to build a computable injective function from reals to lambda terms.

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.

Correct?

Distilled answer:

1. Constructed reals are ok
2. All judgments are perfectly correct except (3)
3. Statement (3) is incorrect because while it is completely ok to talk about algorithms behind each real there is no way to prove that relation from series to corresponding lambda terms left total and right unique, and no way to build a computable injective function from reals to lambda terms.

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?

Distilled answer:

1. Constructed reals are ok
2. All judgments are perfectly correct except (3)
3. Statement (3) is incorrect because while it is completely ok to talk about algorithms behind each real there is no way to prove that relation from series to corresponding lambda terms left total and right unique, and no way to build a computable injective function from reals to lambda terms.