In the first one, they already defined upper bound and least upper bound beforehand, so the statement is more concise than the Strichartz's one. On the other hand, the proof of the completeness axiom, or rather a detailed construction of the reals, is a part I always enjoy in analysis textbooks.

Yes, I have no problem with the fact that the concept "sup A" is defined before the statement of the axiom and then not repeated in it. (It's defined before the statement of theorem 3.1.1 in Strichartz too, it's just also repeated there.) I'm objecting to the fact that they present a theorem as if it were an axiom.

One model's axiom is another model's theorem.

Sure, the proof in Strichartz is constructive, defining a real number that is the supremum of the set.

LLN (I'm going to assume that the family name is Nguyen) can't do that, because they have no model of the real numbers, so it isn't possible to say that some construct is or isn't a real number.

So this is more a case of "what is a theorem if you have a model is only an axiom if you don't".

If you changed the statement of the completeness axiom from "every nonempty subset A of the real numbers that is bounded above has a unique real least upper bound sup A" to "every nonempty subset A of the rational numbers that is bounded above has a unique real least upper bound r", you'd have the Dedekind cut construction of the real numbers. That's not generally presented as an axiom either.

There are sometimes good reasons to define a mathematical object under study (vector space, real numbers, ...) by an axiomatic list of properties it satisfies instead of constructing it from simpler objects. John Conway's ONAG has an interesting mini-chapter about this.

How does Strichartz prove it? You certainly need some axiom beyond, say, the ordered-field axioms; for example, the analogue of Theorem 3.1.1 isn't true for ℚ in place of ℝ.

Strichartz constructs two Cauchy sequences (an increasing sequence starting with a point in E, and a decreasing sequence starting with a point that bounds E above) defined by successive midpoints between the points in each sequence. (That is: take the midpoint between the current top of the increasing sequence and the current bottom of the decreasing sequence, and assign it as the next element of the increasing sequence if it is not an upper bound for E and otherwise the next element of the decreasing sequence.) You can show that

1. These are in fact both Cauchy sequences;

2. They have the same limit;

3. That limit is the supremum of E.

LLN has no definition of a real number, and therefore can only construct real numbers by field arithmetic on other real numbers. That's what's missing.

(I'll take a moment to tangentially observe that I like how my description of the proof neatly explains why it requires the assumptions it does: the theorem requires that E be non-empty because the increasing sequence starts from a point in E, and it requires that E be bounded above because the decreasing sequence starts from an upper bound for E.

If you demand that the sequences start from rational numbers, it's easy to fix the upper bound, but you have to relax the start point of the increasing sequence from "a point in E" to "a point that is not an upper bound for E". That still requires that E is non-empty, but it does it in an awkward, roundabout way.)

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!

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.

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.