Does there exist a proof of the uncountability of the real numbers that uses analytic LLPO (the statement that any real number $x$ satisfies either $x \leq 0$ or $x \geq 0$) but avoids Excluded Middle and the Axiom of Choice (including dependent and countable choice)?
You may use Unique Choice.
I find it difficult to apply LLPO because of the overlapping cases and the unavailability of Countable Choice.
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.
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 directly (without choice and without fLLPO).
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 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$.
This is not an answer but rather an alternative proof of @FrankaWaaldijk's observation that explicit Cauchy sequences are uncountable. The only difference is that we use explicitly given moduli of convergence, rather than a fixed rate of convergence, and that we explicitly impose an equality relation (which I think is implied in @FrankaWaaldijk's answer).
We work in Bishop-style constructive mathematics but without countable choice. In particular, a set is a collection with an imposed equality relation, and a function is an operation that respects the imposed equalities on the domain and the codomain.
Definition: An (explicit) Cauchy sequence is a sequence of rational number $q : \mathbb{N} \to \mathbb{Q}$ together with a strictly increasing function $\mu : \mathbb{N} \to \mathbb{N}$, called modulus, such that $\forall k, m, n \in \mathbb{N} \,.\, |q_{\mu(k) + m} - q_{\mu(k) + n}| < 2^{-k}$. Two Cauchy sequences $(q, \mu)$ and $(q', \mu')$ are considered equal when $|q_{\mu(i)} - q'_{\mu'(j)}| \leq 2^{-i-j}$ for all $i, j \in \mathbb{N}$.
Lemma: There is an operation which takes as input an interval $[\ell, r]$ with rational endpoints and a Cauchy sequence $(q, \mu)$, and outputs an interval $[\ell', r']$ such that $|r' - \ell'| = |r - \ell|/3$ and $[\ell', r'] \subseteq [\ell, r]$, and at most finitely many terms of $q$ are inside $[\ell', r']$.
Proof. We describe the procedure for computing $r'$ and $\ell'$. Let $k$ be the least number such that $2^{-k} < |r - \ell|/12$. Now, if $q_{\mu(k)} > (\ell + r)/ 2$ then let $[\ell', r'] = [\ell, (2 \ell + r)/3]$, otherwise let $[\ell', r'] = [(\ell + 2 r)/3, r]$. In the first case, we have for all $n$ $$ q_{\mu(k)+n} > q_{\mu(k)} - 2^{-k} > (\ell + r)/2 - |r - \ell|/12 > (\ell + 2 r)/3. $$ Thus, at most the first $\mu(k)$ terms of $q$ are contained in $[\ell', r']$. The other case is treated similarly. $\Box$
Theorem: The set of explicit Cauchy sequences is uncountable.
Proof. Let $C$ be the set of all rational Cauchy sequences and $a : \mathbb{N} \to C$ a sequence of Cauchy sequences. We construct a sequence $s$ which avoids every sequence enumerated by $a$.
First, define a sequence of nested intervals $[\ell_{-1},r_{-1}] \supseteq [\ell_0, r_0] \supseteq \cdots$ by taking $[\ell_{-1}, r_{-1}] = [0, 1]$ and letting $[\ell_{k+1}, r_{k+1}]$ be the interval obtained from the Lemma applied to $[\ell_k, r_k]$ and $a(k)$. Now define the sequence $s : \mathbb{N} \to \mathbb{Q}$ by $s_k = (\ell_k + r_k)/2$. By the Lemma, $s_k$ differs from $a(k)_k$ and therefore $s$ is not enumerated by $a$. $\Box$
Authors often require a fixed modulus of convergence for all sequences. For example, Bishop requires $|q_m - q_n| < 1/m + 1/n$ (if memory serves me right), and another popular choice is $|q_m - q_n| \leq 2^{-min(m, n)}$. Which particular modulus we prefer, if any, is not too important because we can always find a subsequence of a given sequence that has any desired modulus:
Lemma: Suppose $(q, \mu)$ is a Cauchy sequence and $\nu : \mathbb{N} \to \mathbb{N}$ a strictly increasing function. Then there is a reindexing function $\iota : \mathbb{N} \to \mathbb{N}$ such that $(q, \mu)$ is equal to $((q \circ \iota), \nu)$.
Proof. Exercise. $\Box$
Of course, one would want to show the uncountability of the set of Cauchy sequences without explicit moduli. That is, suppose we say that $q : \mathbb{N} \to \mathbb{Q}$ is standard Cauchy when $$\forall k \in \mathbb{N} . \exists \mu \in \mathbb{N} . \forall m, n \in \mathbb{N} \,.\, |q_{\mu+m} - q_{\mu+n}| < 2^{-\mu}. \tag{1}$$ Can we show uncountability of standard Cauchy sequences? Well, one seemingly needs to choose a suitable $\mu$ at each step of diagonalization.
However, as a mitigating factor I want to point out that (1) is not a workable definition of Cauchy sequences, unless we do have countable choice, because we cannot even show that a Cauchy sequence of Cauchy sequences converges.
@jkabrg asked whether the explicit Cauchy sequences (with the given equality) form a complete field. I did not verify all the details, but I think the answer is positive so long as one sticks to the principle that without countable choice $\forall\exists$ statements should be replaced by moduli. That is, an explicit Cauchy sequence of explicit Cauchy sequences converges to an explicit Cauchy sequence.
I personally am not a big fan of using setoids, or sets with imposed equality relations. The reason is as follows. Suppose we want to work in a "naturally occurring" constructive mathematical environment $\mathcal{E}$ (a topos, a higher-order fibration, a realizability model, a type theory). Then we do not get to pick equality relations because $\mathcal{E}$ already has a built in notion of equality. If $\mathcal{E}$ also has quotients then we may get the desired equality on a set by quotienting it. Setoids and Bishop's sets-with-equality are not even object of $\mathcal{E}$, but rather objects of an exact completion of $\mathcal{E}_{\mathrm{ex}}$. They live in the wrong place! To put it differently, even though Bishop succeeds in being agnostic about excluded middle, he fails to be ecumenical about equality because he commits to a certain kind of semantic models known as exact completions. These include realizability models but exclude sheaves on a space.
