Weak Archimedean property instead of Archimedean property

Question

We say that a sequence $(z_n)$ of real numbers is a modulated Cauchy sequence, whenever there exists a function $\alpha:\mathbb{N} \rightarrow \mathbb{N}$ such that: $$ |z_i-z_j| \le \frac{1}{k} \quad \forall k \ \forall i,j \ge \alpha(k) . $$ Suppose $(b_n)$ is a sequence of real numbers such that for all $n \in \mathbb{N}$, $|b_{n+1}-b_n| \le \left(\frac{1}{2}\right)^n|x|$ for some $x \in \mathbb{R}$.

I want to constructively prove that $(b_n)$ is a modulated Cauchy sequence, without using the axiom of countable choice. I proved this, using the Archimedean property for real numbers; Here is my proof:

By assumption, for all $n \in \mathbb{N}$, $|b_{n+1}-b_n| \le \left(\frac{1}{2}\right)^n|x|$. By Archimedean property, choose a natural number $l$ such that $|x| < l$. Let $i,j \ge 2lk$. put $n=\min\{i,j\}$, $m=\max\{i,j\}$. We have $$ \begin{split} |b_i-b_j| & =|b_m-b_n| \\ & \le |b_m-b_{m-1}|+|b_{m-1}-b_{m-2}|+\dots+|b_{n+1}-b_n| \\ & \le |x|\left(\frac{1}{2}\right)^{m-1}+|x|\left(\frac{1}{2}\right)^{m-2}+\dots+|x|\left(\frac{1}{2}\right)^{n} \\ & =|x|\frac{1+2+2^2+2^3+\dots+2^{m-1-n}}{2^{m-1}} \\ & =|x|\frac{2^{m-n}-1}{2^{m-1}} =|x|\left(2^{1-n}-\frac{1}{2^{m-1}}\right) \\ & \le l \cdot 2^{1-n} \le l \cdot 2^{1-2lk} \le l \cdot \left(\frac{2}{2^{2lk}}\right) \le l \cdot \left(\frac{2}{2lk}\right) \le \frac{1}{k} \text.\\ \end{split} $$ So $\alpha: \mathbb{N} \to \mathbb{N}$ by $\alpha(k)=2lk$ for all $k \in \mathbb{N}$, is a modulus for $(b_n)$.

My question is, is it necessary to use Archimedean property? I wonder what happens if we substitute Archimedean property with weak Archimedean property that is: $$ \forall x \in \mathbb{R} \neg \neg \exists l \in \mathbb{N} \ x<l $$

My motivation for considering weak Archimedean property instead of Archimedean property is that $\mathbb{R}^e$ ("extended real numbers" or "classical real numbers") described by Troelstra and van Dalen in the book "Constructivism in mathematics", is weakly Archimedean but is not Archimedean.

Answer 1

The Archimedean property in its stronger form is in fact necessary. To see this, consider any real number $ x $ (in your favorite system of real numbers $ \mathbb R $). Let $ b _ n = \frac { | x | } { 2 ^ { n - 1 } } $ for all natural numbers $ n $. Then you have $ b _ n - b _ { n + 1 } = \frac { | x | } { 2 ^ n } $, and therefore $ ( b _ n ) $ is asymptotically regular (see Paulo Oliva's comment). Now, note that if $ ( b _ n ) $ is a Cauchy sequence (regardless of having a modulus), then there is a positive integer $ N $ such that $ b _ N - b _ { N + 1 } \le 1 $, or equivalently $ | x | \le 2 ^ N $. Hence, if every asymptotically regular sequence in $ \mathbb R $ is Cauchy, then $ \mathbb R $ satisfies the stronger form of the Archimedean property.

Answer 2

By the double negation translation, when you replace the assumption $\forall x \exists l (x < l)$ by the weaker $\forall x \neg \neg \exists l (x < l)$, then you should still be able to derive the double negation of the conclusion, i.e., $\neg \neg \forall k \forall i, j \geq \alpha(k) (|z_i - z_j| \leq 1/k)$. In intuitionistic logic one always has $\neg \neg \forall a A(a) \to \forall a \neg \neg A(a)$, so you would actually also have $\forall k \forall i, j \geq \alpha(k) \neg \neg (|z_i - z_j| \leq 1/k)$. If, moreover, you dig into the representation of the reals by sequences of rationals, you'll see that the inequality $|z_i - z_j| \leq 1/k$ is also a universal statement ($\Pi^0_1$). So, intuitionistically it would also be acceptable (via "realizability" interpretation) to conclude the original statement $\forall k \forall i, j \geq \alpha(k) (|z_i - z_j| \leq 1/k)$.