Constructive proof for existence of integer part of real number

Question

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$.

Answer 1

This is an existence and uniqueness proof. Let's first do the case of $x \geq 0$. Let $N_{x}=\{n \in \mathbb{N}\cup \{0\}:x<n+1\}$ We know $N_{x}$ is non-empty because $\lceil x \rceil \in \mathbb{N}$ and $x \leq \lceil x \rceil<\lceil x \rceil+1$ so $\lceil x \rceil+1 \in N_{x}.$ By the well ordering principle, we know $N_{x}$ contains a least element because $N_{x} \subseteq\mathbb{N}$. Let $m+1 \in N_{x}$ be the least element. Since $m+1 \in N_{x}$ we know $x<m+1$. Now for the sake of contradiction suppose $x<m$. Then $m \in N_{x}$ by definition of $N_{x}$. This is a contradiction, because $m<m+1$ yet we already have $\inf(N_x)=m+1$. So we conclude that $x$ is not less than $m$, or equivalently, $x \geq m$.

For uniqueness let's do contradiction again. Suppose there is some other $m'+1 \in N_{x}$ such that $m'\leq x <m'+1$. We already have $m+1$ as the least element of $N_{x}$ so $m'+1>m+1$. Further, as we are dealing with natural numbers we know $m+2 \leq m'+1$, as $m'+1$ must be at least one integer value larger than $m+1$. Clearly $x<m+2$ because $x<m+1$. We also have $m'\leq x$ and $m+1 \leq m'$ is obtained from $m+2 \leq m'+1$. It follows that $m+1<x$. This is a contradiction because we already know $m+1>x$. Thus, no such $m'+1$ can exist: $m+1$ is the unique element that works for our $x \geq 0$.

Now see if you can prove this for $x<0$.

Answer 2

Since $(a_n)_{n=1}^\infty$ is a Cauhy sequence, we have for every rational $\epsilon > 0$ exists a integer $N \ge 1$ such that $| a_j - a_k| \le \epsilon$ for every $j, k \ge N$. Also we have $0 \le a_i - N_i < 1$ for all $i \ge 1$ (integer part for rationals).

Suppose we have a $\epsilon$ such that $$\epsilon < a_j - N_j + \epsilon < 1$$ $$\epsilon < a_k - N_k + \epsilon < 1,$$ so $$-1 < N_j - a_j - \epsilon < -\epsilon$$ $$\epsilon < a_k - N_k + \epsilon < 1$$ $$-\epsilon < a_j - a_k < \epsilon,$$ thus $$-1 < N_j - N_k < 1 \qquad i.e. \qquad N_j = N_k.$$ Now we have $(N_n)_{n=1}^\infty$ converge to the same integer, and so this sequence is a Cauchy sequence equivalent to the integer desired.

To choose such $\epsilon$ we can use the minimal distance from $a_j - N_j, a_k - N_k$ to $1$ such that $$\epsilon < \min (|1 - (a_j - N_j)|, |1 - (a_k - N_k)|).$$

For uniqueness, suppose that $N$ and $N'$ are two integer parts of $x$ real. Since $$0 \le x - N < 1$$ $$0 \le x - N' < 1,$$ so $$-1 < N - x \le 0$$ $$0 \le x - N' < 1.$$ Again, we have $|N - N'| < 1$. Thus $N = N'$.

Answer 3

It suffices to simply consider the set $$ A = \{ n \in \Bbb Z \ | \ n \le x \} $$

By definition $A$ is bounded. Hence $ \sup A $ exists. And by "its" definition the Supremum of a bounded set of real numbers is unique. Now notice your $N = \sup A$ - the proof of which only requires the arguments:

$ N \gt x \implies N - 1 $ is an upper bound for $A$ which is absurd $ \implies N \le x $

$ N + 1 \le x \implies (N + 1 \in A) \; \land ( N + 1 \gt \sup A )$ which too is absurd $ \implies x \lt N + 1 $

Answer 4

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.