Representations of reals in reverse mathematics. (English) Zbl 1138.03012

The author compares four representations of reals as rapidly converging Cauchy sequences, decimal expansions, Dedekind cuts, and open Dedekind cuts. While the statement that a real in any of the above representations can be converted to any other is provable in \(\text{RCA}_0\), it is not so for conversions of sequences. For example, the statement “If \(\langle \lambda_i\rangle_{i\in \omega}\) is a sequence of Dedekind cuts, then there is a sequence \(\langle \sigma_i\rangle_{i\in \omega}\) of open cuts such that, for suitably defined equality of reals, for each \(i\), \(\lambda_i=\sigma_i\),” is equivalent over \(\text{RCA}_0\) to \(\text{ACA}_0\) (showing that the real by real conversion cannot be defined uniformly). For each pair of the representations, Hirst calibrates the proof-theoretic strength of the sequential equivalence, and in each case it turns out to be one of \(\text{RCA}_0\), \(\text{WKL}_0\), or \(\text{ACA}_0\). There are also some interesting related results. For example, for any of the four representations, \(\text{ACA}_0\) is equivalent over \(\text{RCA}_0\) to the statement: If \(\langle \tau_i\rangle_{i\in \omega}\) is a sequence of reals in the specified representation, then the set \(\{i\in\omega: \tau_i \text{ is rational}\}\) exists. There are also reverse mathematics analogs of two theorems of A. Mostowski from [“On computable sequences”, Fundam. Math. 44, 37–51 (1957; Zbl 0079.24702)], concerning change of basis in base representations of sequences of reals.


03B30 Foundations of classical theories (including reverse mathematics)
03F35 Second- and higher-order arithmetic and fragments
03F60 Constructive and recursive analysis


Zbl 0079.24702
Full Text: DOI