The real numbers are a totally ordered field with the least upper bound property (every non-empty set that is bounded above has a least upper bound). The Cauchy sequence or Dedekind cut constructions are existence proofs, not definitions. There is also a uniqueness proof.
Here's a brief informal overview of the Cauchy construction:
A sequence of rationals is a function ##s:\mathbb{N}\rightarrow\mathbb{Q}##. The ##n##th term, ##s_n=s(n)##. So we don't write these functions the same way as usual.
A Cauchy sequence is a sequence ##s## such that for any number ##\epsilon##, we can get ##\vert s_n-s_m\vert <\epsilon## for all the ##n,m\geq N## for some ##N##. In plain language, if we go far enough down the sequence, the rest of the points don't get further apart than ##\epsilon##.
Now, we take all the Cauchy sequences and we identify them as follows. Two Cauchy sequences ##t_n,s_m## are equivalent if given some ##\epsilon>0##, there is always some ##N## such that ##\vert t_n-s_m\vert<\epsilon## for all ##n,m\geq N##. In other words, if we far enough down both sequences, then all the remaining points are within ##\epsilon## of each other.
Since these definitions let ##\epsilon## be any positive rational number, it is helpful psychologically to think of ##\epsilon## being small.
These equivalence classes are going to be our real numbers. We define the operations of addition, multiplication, subtraction, and division of two equivalence classes by taking a sample Cauchy sequence from each, and then doing the respective rational number operation term wise.
It turns out by the triangle inequality that the resulting sequence of rationals is a Cauchy sequence, so it belongs to some equivalence class. It also turns out that no matter which sample Cauchy sequences you choose, you will end up in the same equivalence class at the end. The resulting structure satisfies the field axioms and takes just a little more work to verify that it satisfies the order properties we want.
Note that there are technically no limits or references to infinity used above. Also, we know that there are in fact Cauchy sequences of rationals (constant sequences for instance). An example of a non-constant Cauchy sequence of rationals is ##\frac{1}{n}##.
So far we would have the reals but no proof that there are non-rational reals.
For a cheap proof that there are Cauchy sequences of rationals with no rational limit (hence non-rational reals), the least upper bound of rationals that square to less than ##2## is a real number (by the axioms which are justified by the Cauchy construction), and it squares to ##2## (otherwise it would be too big or too small). There is a classic proof that no rationals square to ##2##.
Note that Wildberger avoids using technical language, as such he is prone to equivocating between what his words mean in common english versus their technical sense.
I just reread your post. Sorry that this is a bit tangential. :-(
