Does the decomposability of $\mathbb{R}$ imply analytic LLPO?

Question

By "BISH" I mean constructive mathematics without axiom of countable choice.

By $\mathbb{R}^f$ I mean real numbers as fundamental sequences of rational numbers and by $\mathbb{R}^d$ I mean real numbers as Dedekind cuts of rational numbers.

By "$dec(X)$" I mean the set $X$ is decomposable which means there exist two inhabited disjoint subsets of $X$, namely $A$ and $B$, such that $X=A \cup B$.

By "sequential $WLPO$" I mean the weak limited principle of omniscience which states that for all binary sequences, either all terms are 0 or this is not the case that all terms are 0.

By $WLPO_{\mathbb{R}^d}$ I mean the weak limited principle of omniscience for $\mathbb{R}^d$, which states that for all $x$ in $\mathbb{R}^d$, either $x=0$ or $\neg(x=0)$.

By $LLPO_{\mathbb{R}^d}$ I mean the lesser limited principle of omniscience for $\mathbb{R}^d$, which states that for all $x$ in $\mathbb{R}^d$, either $x \le 0$ or $x \ge 0$.

I have shown that over BISH, $WLPO_{\mathbb{R}^d}$ ($WLPO_{\mathbb{R}^f}$) implies $dec(\mathbb{R}^d)$ ($\mathbb{R}^f$), which is trivial, and $dec(\mathbb{R}^d)$ ($\mathbb{R}^f$) implies sequential $WLPO$. After that, I proved over BISH, $WLPO_{\mathbb{R}^f}$ and sequential $WLPO$ are equivalent. So I concluded that over BISH, $dec(\mathbb{R}^f)$ and $WLPO$ (analytic or sequential, they are the same here) are equivalent. But we know that over BISH, $WLPO_{\mathbb{R}^d}$ is strictly stronger than sequential $WLPO$. So, my proof implies that $dec(\mathbb{R}^d)$ is weaker than $WLPO_{\mathbb{R}^d}$ and is stronger than sequential $WLPO$. So, there are three possiblities here:

1. $dec(\mathbb{R}^d)$ is strictly between $WLPO_{\mathbb{R}^d}$ and sequential $WLPO$.
2. $dec(\mathbb{R}^d)$ is equivalent to $WLPO_{\mathbb{R}^d}$.
3. $dec(\mathbb{R}^d)$ is equivalent to sequential $WLPO$.

I know that 3 is not the case. Because I have a counter model.

Now, I observe something that may help us to prove that $dec(\mathbb{R}^d)$ implies $WLPO_{\mathbb{R}^d}$. I could show that over BISH, $dec(\mathbb{R}^d)$ and $LLPO_{\mathbb{R}^d}$, implies $WLPO_{\mathbb{R}^d}$. The converse is also true and its proof is trivial. So, over BISH we have "$dec(\mathbb{R}^d)$+$LLPO_{\mathbb{R}^d}$ is equivalent to $WLPO_{\mathbb{R}^d}$". This result was independently interesting to me, because it says that what is the exact logical difference between $WLPO_{\mathbb{R}^d}$ and $LLPO_{\mathbb{R}^d}$ (which we already knew that the latter is strictly weaker than the former). The logical difference is $dec(\mathbb{R}^d)$. Anyway, maybe $dec(\mathbb{R}^d)$ is equivalent to $WLPO_{\mathbb{R}^d}$. In that case, instead of showing that directly, we can try to prove that $dec(\mathbb{R}^d)$ implies $LLPO_{\mathbb{R}^d}$ which seems easier. I tried to show this; i.e I tried to show that $dec(\mathbb{R}^d)$ implies $LLPO_{\mathbb{R}^d}$, but I couldn't succeed. Can anyone help me with this?

Thank you.

---

Answer 1

(To lighten notations, let me simply write $\mathbb{R}$, instead of $\mathbb{R}^d$, for the set of Dedekind reals in what follows, since it is the only one that will appear. For the sake of notational consistency, I will also slightly change the notation for the decomposability of $\mathbb{R}$ to $\mathsf{DEC}(\mathbb{R})$ instead of $\mathit{dec}(\mathbb{R}^d)$.)

I claim that, assuming what is written in the question is correct, $\mathsf{DEC}(\mathbb{R})$ is equivalent to $\mathsf{WLPO}_{\mathbb{R}}$.

To see this, let me first remark that $\mathsf{DEC}(\mathbb{R})$ can be restated as the existence of a function $\chi\colon\mathbb{R}\to\{0,1\}$ such that $\exists a\in\mathbb{R}.\chi(a)=0$ and $\exists b\in\mathbb{R}.\chi(b)=1$. Replacing $\chi$ with $t \mapsto \chi(a+(b-a)t)$ we can assume $a=0$ and $b=1$, i.e., $\chi(0)=0$ and $\chi(1)=1$. Further replacing $\chi$ with $t \mapsto \chi(\inf(1,|t|))$, we can demand $\chi(t)=1$ when $|t|\geq 1$.

Proposition. $\mathsf{DEC}(\mathbb{R})$ together with (sequential) $\mathsf{WLPO}$ imply $\mathsf{WLPO}_{\mathbb{R}}$.

Proof. As remarked above, from $\mathsf{DEC}(\mathbb{R})$ we get a function $\chi\colon\mathbb{R}\to\{0,1\}$ such that $\chi(0)=0$ and $\chi(t)=1$ if $|t|\geq 1$.

Now let $c\in\mathbb{R}$. Define a binary sequence $p_n$ by $p_n = \chi(2^n c)$. If $c\mathrel{\#}0$, meaning $|c|>0$, then $\exists n.(p_n=1)$ (because there exists $n$ such that $2^{-n} \leq |c|$). Contrapositively, if $\forall n.(p_n=0)$ then $c=0$; but the converse is obvious. Thus, $(p_n)$ is the zero sequence iff $c=0$. Now sequential $\mathsf{WLPO}$ tells us that either $(p_n)$ is the zero sequence or it is not, so we get $(c=0) \lor \neg (c=0)$, which is $\mathsf{WLPO}_{\mathbb{R}}$. ∎

Now it is stated in the question (I did not try to prove this myself) that $\mathsf{DEC}(\mathbb{R})$ implies (sequential) $\mathsf{WLPO}$. So, together with the proposition above, this means that $\mathsf{DEC}(\mathbb{R})$ implies $\mathsf{WLPO}_{\mathbb{R}}$. The converse, of course, is obvious (since $\mathsf{WLPO}_{\mathbb{R}}$ asserts that $\mathbb{R}$ is decomposable as the disjoint union of $\{0\}$ and $\{x\in\mathbb{R} : \neg(x=0)\}$). So all of this proves that $\mathsf{DEC}(\mathbb{R})$ is equivalent to $\mathsf{WLPO}_{\mathbb{R}}$, as claimed at the start. (In particular, it implies $\mathsf{LLPO}_{\mathbb{R}}$, answering the titular question.)