Question about construction of $\mathbb{R}$ I hope this question is not naïve, but I've stumbled across it and now it's really bugging me. If we define the real numbers as the completion of the rationals, isn't the statement that every Cauchy sequence converges a tautology? In what sense is it a theorem?
 A: Not quite a tautology, but it does have a very simple proof. See, when we define $\Bbb R$, we effectively replace the copy of $\Bbb Q$, so now you have a Cauchy sequence of reals which are themselves rationals. It is easy to cook the necessary Cauchy sequence of rationals (and prove it is indeed Cauchy), but that's a triviality, not a tautology.
But why should that surprise us? We had $\Bbb Q$ and take $\Bbb R$ as the closure under a certain operation. Why should it be any surprise that the closure is closed? What is slightly more difficult now is to prove that $\Bbb R$ is a Dedekind-complete linear order, i.e. every bounded set has a least upper bound. (More difficult than a triviality, not very difficult in general.)
On the other hand, in many places we define $\Bbb R$ as the Dedekind-completion of $\Bbb Q$, and then you do need to put some work into proving that the result is Cauchy complete. (Some work, not a lot of work.)
A: Many mathematical objects have different, but equivalent characterizations. We often choose just one of them to be the definition, and prove the others as theorems. The definition is then not a theorem. For instance:
Definition: The rational numbers are the quotient field of the integers.
Theorem: The rationals are the unique (up to isomorphism) prime field of characteristic $0$.
But nothing keeps us from doing it the other way around:
Definition: The rationals are the unique (up to unique isomorphism) prime field of characteristic $0$.
Theorem: The rationals are the quotient field of the integers.
In this case, being a prime field is tautologically true for the rationals, while being a quotient field is a theorem. Which of the two ways we choose is really not that important. Important is that the rationals have both characterizations. For this reason, we sometimes switch theorem and definition:
Theorem: A field of characteristic $0$ is prime if and only if it is a quotient field of the integers. Such a field is unique up to unique isomorphism.
Definition: The unique (up to unique isomorphism) field satisfying the above conditions is called the field of rational numbers.
It's mostly about what the author/lecturer thinks is the most important aspect. That's what they'll usually choose as a definition when introducing something to students, barring other considerations.
