The real numbers as a completion of the rationals

Question

The real numbers are the completion (i.e. Cauchy sequences modulo equivalence) of the rational numbers. I want to define the real numbers this way, but without using uniform spaces. The problem is that most definitions I see of metric spaces stipulate that the distance is a function to the real numbers, making this definition circular.

My question is: can we loosen the definition of metric spaces and still retain all (or most) of what we know about metric spaces? e.g. allow the distance function to be a map $$d: X \rightarrow k$$ where $k$ is any totally ordered field? or $k = \mathbb{Q}$? Is there some sense in which every totally ordered field "contains" $\mathbb{Q}$?

One issue that comes to mind is that one can't really talk about "distance preserving morphisms" anymore without fixing $k$.

Answer 1

1. Uniform spaces are your friends.
2. Basically, as André Nicolas commented, you can take $k=\Bbb Q$ first to define the 'metric' whose completion is $\Bbb R$.
3. So, yes, it does make sense to consider metrics $X\times X\to k$ with any totally ordered field, moreover $k$ might also be any totally ordered Abelian (semi-)group.
4. $\Bbb Q$ is present in any field of characteristic $0$, as the subfield generated by $1$.