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.