What is the strength of “if $c≥0$ then $[0,c] = c·[0,1]$” in constructive math (w.r.t., LPO, WLPO, LLPO, etc.)?

Question

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 + c)$ where $c := |a|$, which satisfies $0\leq x\leq c$, 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.

1. [Corrected] The statement that for if $|a|\leq c$ then there is $u\in[-1,1]$ such that $a = c\cdot u$ 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.

Answer 1

I am not sure to what extend an analysis via Weihrauch reducibility (see [1] for an introduction/survey) is of interest to you, but I'll put it forth anyway. The fact that we are finicky about how often a principle is used here might make it easier to translate constructions into a choice-less context than eg arguments in Ishihara/Diener-style constructive reverse mathematics.

In this context, I called $\mathrm{CPO}$ robust division in [2], as it essentially lets us divide by a real number, if it might be $0$. The principle was relevant in the context of analyzing the existence of Nash equilibria in finite two player games. More results are in [3].

Key takeaways: $\mathrm{LLPO}$ is Weihrauch reducible to $\mathrm{CPO}$, but $\mathrm{CPO}$ is not Weihrauch reducible to any finite number of $\mathrm{LLPO}$-applications. $\mathrm{CPO}$ is strictly below both $\mathrm{LPO}$ and $\mathrm{IVT}$ (called "convex choice" $\mathrm{XC}_{[0,1]}$ in much of the Weihrauch reducibility literature).

A Weihrauch equivalent formulation over binary sequences would be: $$\forall p \in \mathbf{2}^\omega \ \exists q \in 2^\omega \ \ (p \neq 0^\omega) \rightarrow \exists k \in \mathbb{N} \ p = 0^k1q$$

[1] V.Brattka, G.Gherardi & A.Pauly: Weihrauch Complexity in Computable Analysis (http://arxiv.org/abs/1707.03202)

[2] A.Pauly: "How non-computable is finding Nash equilibria", JUCS 2010 (https://doi.org/10.3217/jucs-016-18-2686)

[3] T.Kihara & A.Pauly: "Dividing by Zero - How Bad Is It, Really?", MFCS 2016, (https://drops.dagstuhl.de/opus/volltexte/2016/6470/)

Answer 2

Answer

$$\mathbf{IVT} \implies \mathbf{CPO} \implies \mathbf{LLPO}_{\mathbb{R}},$$ where $\mathbf{IVT}$ means Intermediate Value Theorem. Why is this true?

Proposition: $\mathbf{IVT} \implies \mathbf{CPO}$

Proof. Assume $0 \leq x \leq c$. Let $f:[0,1]\to \mathbb R, t \mapsto c\cdot t - x$. We can see that $f(0) \leq 0 \leq f(1)$, so the conditions to apply the IVT hold. We then get that there is a $t \in [0,1]$ such that $f(t)=0$. Rearranging gives $c\cdot t = x$ as desired. Q.E.D.

Improvement assuming Dependent Countable Choice

$$\mathbf{IVT} \iff \mathbf{CPO} \iff \mathbf{LLPO}_{\mathbb{R}}$$

Why? It follows from the following proposition.

Proposition: Assuming Countable Choice, $\mathbf{LLPO}_{\mathbb{R}}$ $\implies$ $\mathbf{IVT}$

Proof. Let $f:[0,1] \to \mathbb R$ be a continuous function satisfying $f(0)\leq0\leq f(1)$. By LLPO, for every rational number $q$ in $[0,1]$, we have $f(q) \geq 0$ or $f(q) \leq 0$. By Countable Choice we obtain a function $P : \mathbb Q \cap [0,1] \to \{0,1\}$ so that $P(q) = 1$ implies $f(q) \geq 0$, and $P(q) = 0$ implies $f(q) \leq 0$. Then using $P$, it is possible to do interval bisection without further application of Countable Choice or LLPO. Q.E.D

Possibility of improvement not assuming Countable Choice?

I'm not sure much is known about what LLPO can do (any version) without Countable Choice. At the moment, $\mathbf{LLPO}_{\mathbb{R}}$ is known to be enough to prove that $\mathbb C$ is closed under square roots, which (I believe) is enough to imply the Fundamental Theorem of Algebra. While there is a constructive proof of FToA by Countable Choice (which can be improved to assume much less; see Richman - The fundamental theorem of algebra: a constructive development without choice) there cannot be an unconditional proof.

Also, if you define:

• $\varepsilon\text-\mathbf{IVT}$ to mean the weakened version of IVT which finds an interval of length $\varepsilon$ containing the root
• $\varepsilon\text-\mathbf{CPO}$ to mean the weakened version of CPO which finds an interval of length $\varepsilon$ containing $t$, given $x$ and $c$

Then we have $\varepsilon\text-\mathbf{IVT} \iff \varepsilon\text-\mathbf{CPO} \iff \mathbf{LLPO}_{\mathbb{R}}$ without any choice.

Why? Observe that while applying choice countably many times is not allowed, it is always allowed to use it finitely many times using induction. It follows that $\mathbf{LLPO}_{\mathbb{R}} \implies \varepsilon\text-\mathbf{IVT}$ because the interval bisection can be carried out for any finite number of iterations, unconditionally.