Context: This question is about constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF. (I wish to avoid the axiom of countable choice if possible, but a partial answer in, say, Bishop-style constructive mathematics — which has dependent choice — is still interesting.) ❧ By “real numbers” (and the set $\mathbb{R}$ of them) I mean the Dedekind reals, as defined in A. S. Troelstra & D. van Dalen, Constructivism in Mathematics (1988), chapter 5, section 5, or in P. Johnstone, Sketches of an Elephant (2002), section D.4.7.
The following principles are standard at least under the assumption of countable choice (in its absence, the subscript $\mathbb{R}$ is used to distinguish them from analogous principles about binary sequences):
$\mathbf{LPO}_{\mathbb{R}}$ is the statement that for all $a\in\mathbb{R}$ we have $a<0$ or $a=0$ or $a>0$.
$\mathbf{WLPO}_{\mathbb{R}}$ is the statement that for all $a\in\mathbb{R}$ we have $a\lessdot 0$ or $a=0$ or $a\gtrdot 0$.
$\mathbf{LLPO}_{\mathbb{R}}$ is the statement that for all $a\in\mathbb{R}$ we have $a\leq 0$ or $a\geq 0$.
— where “$a\lessdot 0$” is defined as “$\neg(a\geq 0)$” (where $a\geq 0$ is itself equivalent to $\neg(a<0)$) and analogously for “$a\gtrdot 0$”. (Note that $a>0$ implies $a\gtrdot 0$ and that the latter implies $a\geq 0$, so $\mathbf{LPO}_{\mathbb{R}}$ implies $\mathbf{WLPO}_{\mathbb{R}}$ and the latter implies $\mathbf{LLPO}_{\mathbb{R}}$.)
Definition: Let me further call $\mathbf{CPO}$ (for “Convexity Principle of Omniscience”, my terminology) the statement that if $c\geq 0$ then $[0,c] = c·[0,1]$, or equivalently:
if $0\leq x\leq c$ then there is $0\leq t\leq 1$ such that $x = c·t$
(it's sufficient to demand that there is $t\in\mathbb{R}$ such that $x = c·t$ because then $t' = 0\sqcup(t\sqcap 1)$ will satisfy $0\leq t'\leq 1$ and still $x = c\cdot t'$, where $\sqcap$ and $\sqcup$ denote the binary inf and sup operations on $\mathbb{R}$).
The question: has the above-defined $\mathbf{CPO}$ been studied in relation to $\mathbf{LPO}_{\mathbb{R}}$, $\mathbf{WLPO}_{\mathbb{R}}$ and $\mathbf{LLPO}_{\mathbb{R}}$ and similar principles? Does it have a standard name? Is it equivalent to one of the three?
To motivate my question, let me show that:
$\mathbf{LPO}_{\mathbb{R}} \Rightarrow \mathbf{CPO}$: We want to show that if $0\leq x\leq c$ then there is $0\leq t\leq 1$ such that $x = c·t$. By $\mathbf{LPO}_{\mathbb{R}}$ we can assume that $c<0$ or $c=0$ or $c>0$. The first case trivially contradicts $c\geq 0$. In the second, we have $x=0$, so $t=0$ works. In the third case, $c$ is invertible (as $\mathbb{R}$ is a Heyting field) so we can let $t = x/c$ which works (and by a remark made above we [can] have $0\leq t\leq 1$).
$\mathbf{CPO} \Rightarrow \mathbf{LLPO}_{\mathbb{R}}$: If $a\in\mathbb{R}$, applying $\mathbf{CPO}$ to $x := \frac{1}{2}(a + |a|)$ and $c := |a|$, we see that¹ there is $-1\leq u\leq 1$ (namely $2t-1$ where $x=c\cdot t$) such that $a = u·|a|$. Now by a fundamental property of the Dedekind reals (Troelstra & van Dalen, op. cit., chapter 5, theorem 5.12(iii)(h)), we have either $u<1$ or $u>-1$. But $u<1$ contradicts $a>0$ (because then $|a|=a$ is invertible so necessarily $u=1$), in other words, $u<1$ implies $a\leq 0$, and similarly $u>-1$ implies $a\geq 0$. So we have $a\leq 0$ or $a\geq 0$, as claimed.
- The statement that for all $a\in\mathbb{R}$ there is $u\in[-1,1]$ such that $a = u·|a|$ is, in fact, clearly equivalent to $\mathbf{CPO}$ and maybe more satisfactory.
I have not been able to prove the converse of one of these two implications, nor to relate $\mathbf{CPO}$ with $\mathbf{WLPO}_{\mathbb{R}}$, hence my question.
I also didn't find the statement I called $\mathbf{CPO}$ above in Hannes Diener's long text on “Constructive Reverse Mathematics”, though of course I may have missed it, but I'd be surprised if it hasn't been considered (and named) before.
