Existence of sequence of rational numbers in $RCA_0$

Question

In subsystem $RCA_0$ of second order arithmetics, existence of arbitrary functions is not guaranteed since some may not be defined using $\Delta_1^0$ comprehension. In Simpson's book, when real numbers are developed, sequences of rational numbers come in. Is there any validation of the existence of sequences of rational numbers within $RCA_0$? If not, why could we develop the real number system within $RCA_0$ in this way?

Answer 1

Here a real number is any sequence $(q_n)$ of rational numbers such that $(\forall n)(\forall i)(|q_{n + i } - q_{i }| < 2^n$.

Let $(M,S)$ denote a model of second order arithmetic, where S denote the second order part. The real numbers of the particular model (M,S) are those sequences of rational satisisfying the above property that happen to be in $S$.

In some models you have real with certain properties and in other models you may not have those reals. For example, (from Simpson's book) over $RCA_0$, $ACA_0$ is equivalent to the image od any closed subset of $[0,1]$ under any continuous real value function has a supremum. So if $(M,S)$ is a model of $RCA_0$ which is not a model of $ACA_0$, like REC, then there is a real number with a certain property missing that every model of $ACA_0$ would have.

You can developed the real number system in $RCA_0$. The real numbers are just those sequence that happen to exist. However because of this some of the familiar property of the real numbers may not be proveable. The interesting question is what subsystems can prove these properties and is the property with $RCA_0$ equivalent to a familiar subsystem. In this way, reverse math attempts to classify theorem of mathematics according to their proof strength.