Return to Answer

The answer is in spirit: yes. One can prove uncountability of the reals without using countable choice by using a modified version of LLPO which I call fLLPO (functional LLPO).

The answer is in spirit: yes. One can prove uncountability of the reals without using countable choice by using a modified version of LLPO which I call fLLPO (functional LLPO).

In my view, constructive uncountability of the reals relies on countable choice only indirectly.

But if we define the reals numbers a bit more precise, as is common practice for instance in intuitionistic mathematics INT, then uncountability follows without choice (or from unique choice, whichever view you prefer).

Corollary (without choice): The set of real numbers $\mathbb{R}$ contains an uncountable subset.

The answer is in spirit: yes. One can prove uncountability of the reals without using countable choice by using a modified version of LLPO which I call fLLPO (functional LLPO).

Still, fLLPO is also not essentially necessary in my opinion. In my view, constructive uncountability of the reals relies on countable choice only indirectly.

But if we define the reals numbers a bit more precise, as is common practice for instance in intuitionistic mathematics INT, then uncountability follows directly (without choice and without fLLPO).

Corollary (without choice): The set of real numbers $\mathbb{R}$ contains the uncountable subset $E$ of explicit reals.

But we would like to see that this subset $E$ is in fact all of $\mathbb{R}$, in the sense that any real number is equivalent to an explicit real.

For this we can use a functional version of LLPO called fLLPO, and for clarity we need to look at the representation of real numbers through Cauchy-sequences. We will call the set of Cauchy-sequences $\mathbb{R}_{\rm basis}$.

fLLPO (functional Lesser Limited Principle of Omniscience)
There is a function $f_{\geq 0}:\mathbb{R}_{\rm basis} \rightarrow \{0,1\}$ such that for all $x\in \mathbb{R}_{\rm basis}$ we have $f_{\geq 0} (x) = 0 \rightarrow x\leq 0$ and $f_{\geq 0} (x) =1 \rightarrow x \geq 0$

Notice that according to Bishop, if we assume LLPO then such a function should exist by the very meaning of $\forall\exists$.

Proposition (using fLLPO): Every real number is equivalent to an explicit real number.

proof (short version, I will fill in later)
For a given $x\in \mathbb{R}_{\rm basis}$ we can apply the function $f_{\geq 0}$ step-by-step to determine uniquely an explicit real $y$ equivalent to $x$.

In my view, constructive uncountability of the reals relies on countable choice only indirectly.

Generally speaking, countable choice is mostly needed in situations where we prefer to keep our objects slightly generic, to help our 'bookkeeping' remain light.

But if we define the reals numbers a bit more precise, as is common practice for instance in intuitionistic mathematics INT, then uncountability follows without choice (or from unique choice, whichever view you prefer).

To see this, take the following

Definition of the explicit reals:
A sequence $x=[l_0,r_0],[l_1,r_1],\ldots$ of binary rational intervals is an explicit real number iff for all $n\in\mathbb{N}$ we have

• $r_n, l_n\in 2^{-n}\cdot\mathbb{Z}$

• $r_n-l_n=2^{-n+1}$

• $[l_{n+1},r_{n+1}]\subset[l_n,r_n]$

This definition can be a bit cumbersome, for instance when multiplying explicit real numbers, because it forces one to specify any real number with a strict convergence rate.

And, given a Cauchy sequence of rationals $c$ which has no explicit modulus of convergence, one needs countable choice to see that $c$ is Cauchy-equivalent to an explicit real number. This is in my opinion the indirect reason why countable choice is 'necessary' to prove uncountability of the real numbers (given by the Cauchy-sequence definition).

The other way round is choice-unproblematic: any explicit real $x$ determines a unique Cauchy-sequence of rationals, just take the left end points $(l_n)_{n\in\mathbb{N}}$.

Now the explicit real numbers are easily seen to be uncountable without using choice, through a simple diagonal argument.

Proposition (without choice): the explicit reals are uncountable.

proof Let $x_0, x_1,\ldots$ be a sequence of explicit reals. Then we can construct an explicit real $y=[s_0,t_0],[s_1,t_1],\ldots$ such that $y\# x_n$ for all $n\in\mathbb{N}$.

To see this, firstly we put $s_0=0, t_0=2$.

Next, suppose that for given $n$, the left and right end points $s_{2i+1}, t_{2i+1}, s_{2i+2}, t_{2i+2}$ have been defined for all $i< n$, such that moreover $[s_{2i+2}, t_{2i+2}]\ \#\ x_i$.

We now consider the left and right end points of $(x_n)_{2n+2}$, which is the $2n\!+\!2$ -th binary interval of the sequence $x_n$. Call those end points $u_{2n+2}, v_{2n+2}$ respectively, then $v_{2n+2}-u_{2n+2}=2^{-2n-1}$ since $x_n$ is an explicit real.

Since $t_{2n}-s_{2n}=2^{-2n+1}$, there are a unique smallest binary rational $q\in 2^{-2n-2}\cdot\mathbb{Z}$ and a subsequent unique smallest binary rational $r\in 2^{-2n-1}\cdot\mathbb{Z}$ such that

(i) $[q,q+2^{-2n-1}]\subset [s_{2n}, t_{2n}]$

(ii) $[q,q+2^{-2n-1}]\ \# \ [u_{2n+2}, v_{2n+2}]$

(iii) $[q,q+2^{-2n-1}]\subset [r,r+2^{-2n}]\subset [s_{2n}, t_{2n}]$

We can now define $s_{2n+1}=r, t_{2n+1}=r+2^{-2n}$ and $s_{2n+2}=q, t_{2n+2}=q+2^{-2n-1}$.

We leave it to the reader to verify that $y=[s_0,t_0],[s_1,t_1],\ldots$ is a well-defined explicit real number such that $y\# x_n$ for all $n\in\mathbb{N}$.

In my view, constructive uncountability of the reals relies on countable choice only indirectly.

Generally speaking, countable choice is mostly needed in situations where we prefer to keep our objects slightly generic, to help our 'bookkeeping' remain light.

But if we define the reals numbers a bit more precise, as is common practice for instance in intuitionistic mathematics INT, then uncountability follows without choice (or from unique choice, whichever view you prefer).

To see this, take the following

Definition of the explicit reals:
A sequence $x=[l_0,r_0],[l_1,r_1],\ldots$ of binary rational intervals is an explicit real number iff for all $n\in\mathbb{N}$ we have

• $r_n, l_n\in 2^{-n}\cdot\mathbb{Z}$

• $r_n-l_n=2^{-n+1}$

• $[l_{n+1},r_{n+1}]\subset[l_n,r_n]$

This definition can be a bit cumbersome, for instance when multiplying explicit real numbers, because it forces one to specify any real number with a strict convergence rate.

And, given a Cauchy sequence of rationals $c$ which has no explicit modulus of convergence, one needs countable choice to see that $c$ is Cauchy-equivalent to an explicit real number. This is in my opinion the indirect reason why countable choice is 'necessary' to prove uncountability of the real numbers (given by the Cauchy-sequence definition).

The other way round is choice-unproblematic: any explicit real $x$ determines a unique Cauchy-sequence of rationals, just take the left end points $(l_n)_{n\in\mathbb{N}}$.

Now the explicit real numbers are easily seen to be uncountable without using choice, through a simple diagonal argument.

Proposition (without choice): the explicit reals are uncountable.

proof Let $x_0, x_1,\ldots$ be a sequence of explicit reals. Then we can construct an explicit real $y=[s_0,t_0],[s_1,t_1],\ldots$ such that $y\# x_n$ for all $n\in\mathbb{N}$.

To see this, firstly we put $s_0=0, t_0=2$.

Next, suppose that for given $n$, the left and right end points $s_{2i+1}, t_{2i+1}, s_{2i+2}, t_{2i+2}$ have been defined for all $i< n$, such that moreover $[s_{2i+2}, t_{2i+2}]\ \#\ x_i$.

We now consider the left and right end points of $(x_n)_{2n+2}$, which is the $2n\!+\!2$ -th binary interval of the sequence $x_n$. Call those end points $u_{2n+2}, v_{2n+2}$ respectively, then $v_{2n+2}-u_{2n+2}=2^{-2n-1}$ since $x_n$ is an explicit real.

Since $t_{2n}-s_{2n}=2^{-2n+1}$, there are a unique smallest binary rational $q\in 2^{-2n-2}\cdot\mathbb{Z}$ and a subsequent unique smallest binary rational $r\in 2^{-2n-1}\cdot\mathbb{Z}$ such that

(i) $[q,q+2^{-2n-1}]\subset [s_{2n}, t_{2n}]$

(ii) $[q,q+2^{-2n-1}]\ \# \ [u_{2n+2}, v_{2n+2}]$

(iii) $[q,q+2^{-2n-1}]\subset [r,r+2^{-2n}]\subset [s_{2n}, t_{2n}]$

We can now define $s_{2n+1}=r, t_{2n+1}=r+2^{-2n}$ and $s_{2n+2}=q, t_{2n+2}=q+2^{-2n-1}$.

We leave it to the reader to verify that $y=[s_0,t_0],[s_1,t_1],\ldots$ is a well-defined explicit real number such that $y\# x_n$ for all $n\in\mathbb{N}$.

In slightly more general phrasing we therefore find:

Corollary (without choice): The set of real numbers $\mathbb{R}$ contains an uncountable subset.