# Existence of sequence of rational numbers in $RCA_0$

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?

-
Recursive comprehension is sufficient to establish the existence of some such sequences. In chapter II this is all developed in detail. – Benedict Eastaugh Aug 28 '12 at 18:40
You mean $\Delta^0_1$ rather than $\Delta^1_0$. – Carl Mummert Aug 28 '12 at 19:14
@CarlMummert: Thanks! You are right! – Jing Zhang Aug 28 '12 at 21:06
@BenedictEastaugh: Therefore, it does not ensure the existence of all real numbers then? – Jing Zhang Aug 28 '12 at 21:10
Correct. @William has gone into the details of this in his answer below. – Benedict Eastaugh Aug 29 '12 at 10:10

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.
Very nice answer. Is it correct to say that although within $RCA_0$ a real number is defined as a sequence of rational numbers with some properties, not every real number is guaranteed to exist within $RCA_0$? – Jing Zhang Aug 28 '12 at 21:14
@Jing Zhang: yes, $\mathsf{RCA}_0$ does not guarantee the existence of every real number - but neither does any other countable theory in first order logic, including ZFC. It has nothing to do with the theory, it's just a consequence of the Lowenheim-Skolem theorem. – Carl Mummert Aug 28 '12 at 21:31