As per Michael J. Schramm, 1996, Introduction to real analysis, Theorem 6.6:
In an Archimedean ordered field in which the Nested Intervals property holds, there is a one-to-one correspondence between the interval $I = (0, 1]$ and the nonterminating decimal expansions of the form $0.d_1 d_2 d_3 …$
The proof is based on nested intervals and uses a procedure with infinite number of steps.
Is there known way to proof this theorem not using infinite procedure?
7/23/2022
It seems my question needs some clarification.
I was looking into multiple textbooks for real analysis, and there were a few that made the effort to prove the equivalence of these two sets. Most were just mentioning about it, almost like an axiom. And since by definition the decimal real number is an infinite string of digits, there is always an infinite procedure involved that would map the real number to the string. The procedure itself in some sources is described explicitly, like in Michael J. Schramm, in some it is assumed implicitly.
Let have as an example how the problem is treated in Introduction to Real Analysis by Jirí Lebl, 2018.
Let's consider only real numbers in the interval $I = \left(0, 1\right]$. Take an infinite sequence of decimal digits $0.d_1 d_2 d_3 …$ where there is a digit $d_j$ for every $ j \in \mathbb{N}$ and define
$D_n := \frac {d_1}{10}+\frac {d_2}{10^2}+\frac {d_3}{10^3} + ... + \frac {d_n}{10^n}$
as the truncation of $x$ to $n$ decimal digits. We say then that this sequence of digits represents a real number $x$ if
$x = sup \{ D_n : n \in \mathbb{N} \}$.
${Proposition \; 1.5.1}$
i) Every infinite sequence of digits $0.d_1 d_2 d_3 … $ represents a unique real number $x \in [0, 1]$, and
$D_n \leq x \leq D_n + \frac {1}{10^n}$ for all $n \in \mathbb{N}$
ii) For every $x \in (0, 1]$ there exists an infinite sequence of digits $0.d_1 d_2 d_3 …$ that represents $x$.
If following relation holds:
$D_n < x \leq D_n + \frac {1}{10^n}$ for all $n \in \mathbb{N}$
then the representation for $x$ is unique.
The proof of the first part follows directly from the definition.
The proof of the existence is based on the Archimedean property and uses strong induction.
The procedure how to define the next digit is not shown explicitly, it is just proven that there exists integer $j$ such that
$(j - 1) 10 ^{-(n+1)} < x - D_n \leq j 10^{-(n+1)}$
The uniqueness, again, follows from the definition and the conditions:
$D_n < x \leq D_n + \frac {1}{10^n}$ for all $n \in \mathbb{N}$
which in fact states that all the digits $d_n$ are uniquely defined by the procedure above.
What is my problem with that kind of proof - first, it involves an infinite number of steps, as well as conditions, and second, in order to verify any of the conditions one needs to have a way to compare $x$ to the current truncated value $D_n$. Obviously, $D_n$ is a decimal number, but what is $x$?
The whole proof looks like a Gedankenexperiment. Is that a valid proof?