# DLO’s III – from rational to real

From the last two posts we managed to prove both the existence and the uniqueness of the rationals, which could be done by explicit definitions using known facts about the natural numbers. However, we also showed that the property that distinguished the real numbers from the rationals, namely completeness, couldn’t be defined in first-order logic. This also means that we can’t proceed to prove the existence of the reals in a direct matter as the rationals, and we will do so by indirect means. Continue reading

Now that we’ve proven that the rationals exist, we would like to know if it would make a difference had we picked another representative of the countable DLO’s without endpoints as our rationals. Would any candidate have been suitable or is our choice of $\left<\mathbb{Q},\prec_\mathbb{Q}\right>$ special? Continue reading