Question about Lemma (2.3) in Constructive Analysis, Bishop and Bridges

Question

I am in the process of formalizing the constructive notion of a real number and the equivalence on them in the proof assistant Agda, but I am having trouble with the proof of Lemma (2.3) in the following:

In Errett Bishops and Douglas S. Bridges Constructive Analysis from 1985, real numbers are constructively defined as a regular sequence of rational numbers, where regularity of a sequence $x \equiv x_n$ is defined as

$$|x_n - x_m|\leq m^{-1} + n^{-1}$$ For any strictly positive integers $n, m$.

And equivalence as

Two real numbers $x \equiv (x_n)$ and $y \equiv (y_n)$ are equal if \begin{equation} | x_n - y_n| \leq 2n^{-1} \end{equation} For all strictly positive integers n.

Lemma (2.3) The real numbers $x\equiv(x_n)$ and $y\equiv(y_n)$ are equal if and only if for each positive integer $j$ there exists a positive integer $N_j$ such that $$|x_n - y_n| \leq j^{-1} \quad (n > \geq N_j)$$ Proof: If $x=y$ then the lemma holds with $N_j \equiv 2j$ Assume conversly that for each positive integer j there exists an $N_j$ satisfying the relation. Consider a positive integer $n$. If $m$ and $j$ are any positive integers with $m \geq max(j, N_j)$ then $$ > |x_n - y_n| \leq |x_n - x_m| + |x_m - y_m| + |y_m - y_n| \leq n^{-1}+ > m^{-1} + j^{-1} + m^{-1} + n^{-1} < 2n^{-1} + 3j^{-1}$$ Since this holds for any positive integer j, then x and y are equivalent.

The very last part of this proof is what I am having difficulties with. I understand that we can, informally (and perhaps classically?) let $j$ go infinity (although this is hard to express formally in the current framework I'm using) and let $3j^{-1}$ vanish. But how are we to, given an n, constructively choose a j and complete the proof of this lemma?

If it holds for all j, shouldn't it be true in particular for $j = 1$ for example?

Can someone shed some light on this?

Answer 1

Yes, the inequality holds for all $j$. Indeed, for all $j$ (included $j=1$ or whatever) we can choose an auxiliar $m$ satisfaying $m\geq\max(j,N_j)$, for example $\max(j,N_j)$ itself is valid. Independiently of $m$ chosen (given $j$), we have necessarily

$|x_n-y_n|\leq 2 n^{-1} + 3 j^{-j}$ for all $j$.

This implies that $|x_n-y_n|\leq 2 n^{-1}$ (you can proceed by way of contradiction).

Answer 2

Recall that $x$, $y$, and $n$ are rational. For rational numbers, in systems like Bishop's framework for constructive mathematics, we retain much of classical logic. For example, we know in Bishop's system that if $p$ and $q$ are rational then exactly one of $p < q$, $p = q$, or $p > q$ holds. Indeed, if you give me two rational numbers I can determine constructively which of these is the case.

So, even working constructively, I can work by assuming that $|x_n - y_n| \geq 2n^{-1}$ and obtaining a contradiction. The same technique as the classical proof will work here. If $|x_n - y_n| > 2n^{-1}$ then we can constructively find a $j$ small enoungh that $|x_n - y_n| > 3j^{-1} + 2n^{-1}$, which is a contrdiction to the inequality established already in the proof.

One place that a difference will occur with Bishop's system is with real numbers. In Bishop's system, we do not know that for all real numbers $r,s$ we have $r < s$, $r = s$, or $ r > s$, so we cannot prove $r < s$ by showing that $r \geq s$ leads to a contradiction. But we can use that method for natural numbers or rational numbers.