Equivalence of omniscience principles for natural numbers and analytic omniscience principles for Cauchy real numbers

Question

In constructive mathematics, a proposition $P$ is decidable if $P \vee \neg P$, and a proposition is stable if $\neg \neg P \implies P$. We have the following principles of omniscience for the natural numbers: Given any decidable predicates $\phi$ and $\psi$ on the natural numbers; i.e. one such that for all natural numbers $n$, $\phi(n)$ or $\neg \phi(n)$, and $\psi(n)$ or $\neg \psi(n)$

• The limited principle of omniscience ($\mathrm{LPO}_\mathbb{N}$) for the natural numbers state that the existential quantifier $\exists n \in \mathbb{N}.\phi(n)$ is decidable

• The weak limited principle of omniscience for the natural numbers ($\mathrm{WLPO}_\mathbb{N}$) state that the universal quantifier $\forall n \in \mathbb{N}.\phi(n)$ is decidable

• Markov's principle for the natural numbers ($\mathrm{MP}_\mathbb{N}$) state that the existential quantifier $\exists n \in \mathbb{N}.\phi(n)$ is stable

• The lesser limited principle of omniscience ($\mathrm{LLPO}_\mathbb{N}$) for the natural numbers states that if it is not the case that both existential quantifiers $\exists n \in \mathbb{N}.\phi(n)$ and $\exists n \in \mathbb{N}.\psi(n)$ hold, than either $\neg \exists n \in \mathbb{N}.\phi(n)$ or $\neg \exists n \in \mathbb{N}.\psi(n)$.

There are also the following analytic principles of omniscience for the Cauchy real numbers (i.e. equivalence classes of Cauchy sequences of rational numbers with modulus of convergence):

• The analytic limited principle of omniscience for Cauchy real numbers state that the Cauchy real numbers have decidable apartness.

• The analytic weak limited principle of omniscience for Cauchy real numbers state that the Cauchy real numbers have decidable equality.

• The analytic Markov's principle for Cauchy real numbers state that the Cauchy real numbers have stable apartness.

• The analytic lesser limited principle of omniscience for Cauchy real numbers state that the partial order on the Cauchy real numbers defined by the negation of the strict order $\lt$ is a total order.

Are the two sets of omniscience principles equivalent to each other? i.e.

• Is $\mathrm{LPO}_\mathbb{N}$ equivalent to analytic LPO for Cauchy real numbers?

• Is $\mathrm{WLPO}_\mathbb{N}$ equivalent to analytic WLPO for Cauchy real numbers?

• Is $\mathrm{MP}_\mathbb{N}$ equivalent to analytic Markov's principle for Cauchy real numbers?

• Is $\mathrm{LLPO}_\mathbb{N}$ equivalent to analytic LLPO for Cauchy real numbers?

Answer 1

Let me try to tackle the LPO case. I will even try to show that it doesn't matter whether we assume our Cauchy sequences to have a modulus or not. (Please check me carefully because I know I've made mistakes on similar questions before.)

The easy direction is to prove that LPO for Cauchy reals (with or without modulus) implies LPO for natural numbers. To this effect, let $b\colon\mathbb{N}\to\{0,1\}$ and we wish to show that either $\exists n.(b(n)=1)$ or that $\forall n.(b(n)=0)$. Define $u_n \in \mathbb{Q}$ as $\sum_{k=0}^{n} 2^{-k}\,b(k)$. Clearly this is Cauchy-with-explicit-modulus, so it defines a real $x$ (viꝫ. the limit of $(u_n)$): by LPO on the Cauchy reals (with or a fortiori without modulus), we have either $x\mathrel{\#}0$ (“is apart from”) or $x=0$. In the former case, $x>2^{-k}$ for some $k$ so it is easy to see that some $b(n)=1$, and in the latter case, clearly $b(n)=0$ for all $n$. ∎

Now for the other direction. We assume LPO for natural numbers. Let $x$ be a Cauchy real, defined as the limit of a sequence $(u_n)$ of rationals, which we do not assume to have a modulus so as to have the most general result. We want to show that $x\mathrel{\#}0$ or that $x=0$. For notational convenience, we assume w.l.o.g. (replacing $u_n$ by $|u_n|$ and $x$ by $|x|$) that $u_n\geq 0$ and $x\geq 0$, so now we want to show that $x>0$ or that $x=0$.

Let $k,n\in\mathbb{N}$. By LPO for the natural numbers (and because comparisons of rationals are decidable), either $u_m > 2^{-k}$ for some $m\geq n$ or $u_m \leq 2^{-k}$ for all $m\geq n$. Since these two cases are exclusive, we can define $b(k,n)=1$ in the former and $b(k,n)=0$ in the latter.

Now let $k\in\mathbb{N}$ (but allow $n$ to vary). By a second application of LPO on the natural numbers, either there is $n$ such that $b(k,n)=0$ or we have $b(k,n)=1$ for all $n$. Again, these two cases are exclusive, so we can define $b(k)=0$ in the former and $b(k)=1$ in the latter.

Now by a third application of LPO on the natural numbers, either there is $k$ such that $b(k)=1$ or we have $b(k)=0$ for all $k$.

This shows that either $\exists k. \forall n. \exists m\geq n. (u_m > 2^{-k})$ or $\forall k. \exists n. \forall m\geq n. (u_m \leq 2^{-k})$. In the former case we have $x\geq 2^{-k}$ so $x>0$. In the latter case, we have $x=0$. ∎

PS [added in edit]: in the above, I wanted to show that LPO for natural numbers implies LPO for Cauchy reals even without modulus; but since the question was about Cauchy reals with modulus, I should point out that the proof (of the second part) simplifies: if we assume $|u_p-u_q|\leq 2^{-n}$ when $p,q\geq n$, then $x>0$ is equivalent to $\exists n.(u_n>2^{-n})$ and $x=0$ to $\forall n.(u_n\leq 2^{-n})$, so we need to show that either the former or the latter holds, and that is a single application of LPO for $\mathbb{N}$.