I try to prove de following exercise of my analysis textbook.
Show that for every real number $x$ there is exactly one integer $N$ such that $N \le x < N + 1$.
I have been finding a constructive proof by Cauchy sequence definition and the lemma of integer part for rational: for every rational number $x$ there is exactly one integer $N$ such that $N \le x < N + 1$. So if $(a_n)_{n=1}^\infty$ is a Cauchy sequence then exists a integer $N_i$ such that $N_i \le a_i < N_i + 1$ for all $i \ge 1$.
Best Answer
The unfortunate fact is that the result in question cannot be proved constructively.
Here "constructive proof" as usual means "a proof using the methods that are acceptable in mathematical constructivism".
If this result could be prove constructively, then we would have a constructive proof that there is a total function $f(x) = N$ from $\mathbb{R}$ to $\mathbb{N}$, where $N$ is the unique integer with $N \leq x < N+1$. But that function is discontinuous, and any function from the real line that we can form constructively will be continuous.
In fact, any function from $\mathbb{R}$ to $\mathbb{N}$, which we can prove constructively is a function, must be constant. See the section 'The continuum' in this Stanford Encyclopedia entry.
It may be easier to think of the following issue, which is the root cause of the facts above. Suppose that we have a quickly-converging Cauchy sequence of rationals, $(a_n)$, that converges to a real $x$. We want to read off $f(x)$ by looking at the entries of $(a_n)$. Suppose that we see $a_k = 1-2^k$ for all the vales of $k$ we have examined. Then the sequence $(a_n)$ might continue its pattern forever, converging to $1$. Or, perhaps, at some moment, the sequence $(a_n)$ could jump "above" $1$ or jump "below" 1. So the evaluation map that takes a quickly converging Cauchy sequence $(a_n)$ and produces $f(\lim a_n)$ will not be continuous. That is the real obstacle to a constructive proof of this result, assuming the reals are defined as Cauchy sequences.