News for hackers. Stuff that matters.
Re:Real Not Complex: Free Math Resources by JadeNB on Saturday March 28, 2020 @04:59PM (#22714291)
Yes, fair enough: it fits more naturally into the general context of metric spaces to come to postulate the completeness of ℝ as a metric space and prove its completeness as an ordered space, rather than the other way around. Of course, one still does have to have a completeness postulate in some sense!
Re:Real Not Complex: Free Math Resources by thaumasiotes on Saturday March 28, 2020 @07:07PM (#22714988)
Theorem 2.3.1 (Completeness of the Reals) A sequence x_1, x_2, ... of real numbers has a limit if and only if it is a Cauchy sequence.

(The wording is unfortunate in this context as stated, but the proof shows that the limit of a Cauchy sequence of reals exists and is itself a real number as opposed to some other kind of thing.)

Completeness is something we want; a lot of effort goes into proving that we've actually achieved it.

The fact that Theorem 2.3.1 is given a name does suggest, though, that Strichartz agreed with you as to which kind of completeness was more significant.

Re:Real Not Complex: Free Math Resources by JadeNB on Saturday March 28, 2020 @07:32PM (#22715131)
I was about to ask how he proves that, but that way lies an infinite regress, so I found a copy and checked. I see that he defines (without using the terminology) the real numbers to be the completion of the rational numbers for the usual Archimedean metric and so, as you say, is able to prove the completeness rather than postulating it. (This explains to me your remark elsethread (https://news.ycombinator.com/item?id=22712940) that "So this is … a case of 'what is a theorem if you have a model is only an axiom if you don't'.", which I didn't understand on first reading.)

Note that this is just a difference of terminology from other approaches; those approaches prove properties of an abstract object satisfying certain axioms, and then are obliged to exhibit a specific such object. The approach you favour is definitely more hands-on, but runs the risk of obscuring that really field axioms + uniqueness is all we need; if someone else prefers to construct their reals using, say, Dedekind cuts, then there is no need to check all the theorems proven along the way, only that the axioms of a complete (as an ordered or metric space) ordered field still hold.