Earlier, I posted a pretending-to-be-funny discussion on this subject and now continue in a more formal fassion. Namely the dialogue in the previous post didn’t actually arrive to any conclusion as to whether 0.9999… is 1 or not. When you want to prove something in mathematics, you need to look down at the definitions as was suggested in the dialogue. In what follows, I take the axioms of an ordered field with the completeness axiom as the definition of the real numbers, that is the most common definition and equivalent to all others as long as the object is called real numbers and cook up a proof of…..
Theorem.
.
Proof.
Let us review the axiomatization of the real numbers. The vocabulary is
. All axioms except one are first-order sentences over this vocabulary and one is second-order (
in fact). The symbols
and
are constants and
and
are functions.
Remark
We use the conventional logic way of presenting the axioms (talking about vocabulary etc.). Instead we could plainly state that for each
and
there exists a unique number denoted by
, same for
, and then list the following axioms. Constant symbols
and
are taken only for convenience since they are definable from
and
and these definitions define unique elements in the theory below.
The axioms are the axioms of a non-trivial commutative ordered field plus the axiom of completeness:
Axiom 1: 
Axiom 2: 
Axiom 3: 
Axiom 4: 
Axiom 5: 
Axiom 6: 
Axiom 7: 
Axiom 8: 
Axiom 9: 
Axiom 10: 
Axiom 11: 
Axiom 12: 
Axiom 13: 
Axiom 14: 
Axiom 15: 
Axiom 16: 
Axiom 17: Let
be a unary second order variable. The completeness axiom states:


![\exists x\big(\forall y(R(y)\rightarrow x\ge y)\land \forall y<x\exists z(R(z)\land y<z<x)\big)\big]\big]. \exists x\big(\forall y(R(y)\rightarrow x\ge y)\land \forall y<x\exists z(R(z)\land y<z<x)\big)\big]\big].](/wp-content/plugins/latexrender/pictures/9cf9d3e3b815eb24036e8cbfe896582d.png)
In words, all non-empty subsets
which have an upper bound, have also the smallest (least) upper bound.
Note that the axiom of completeness 17 does not say whether the smallest upper bound is unique. That will be needed:
Claim 1
Let
be a set with an upper bound. Then there exists a unique
which is the least upper bound.
Proof of Claim 1
Suppose
and
are two upper bounds:


If we show that neither
nor
holds, then by axiom 13 it will follow that
. Suppose that
. Then substituting
in place of
we get as a consequence

which implies that
is not an upper bound which is a contradiction. Similarly if
, then by substituting
in place of
in
we get that
is not an upper bound which is a contradiction again.
To proceed, we must define
. I choose to define it in the following way which is equivalent to all conventional ways:
Definition
is the unique least upper bound of the set

where:
is the set of natural numbers,
, the operation
is recursively definable by
and
and the operation
gives the unique element given by axiom 7 (uniqueness proof uses also axioms 5 and 6: exercise).
In the definition above I deliberately use the existence of
. It can be justified as follows. First, if we assume the non-existence of
, then (the axioms of set theory, other than the infinity axiom, imply that) the set of axioms 1–16 is inconsistent (exercise). Second, we already assumed the existence of the infinite sequence of symbols
which, to put it mildly, is hard to maintain without the existence of
.
Once we prove that
is a smallest upper bound for the set
, Claim 1 implies that
. In order to prove that, we need to show that the sentence
in the beginning of the proof with
replaced by
and
replaced by
holds. Suppose
. Then for some
,
. By axioms 4, 10 and 15,
which implies
, where subtraction is the addition of the additive inverse whose existence follows from axiom 3. By the same axioms we get
. Multiplying both sides by
and applying axiom 9 we get
which, after applying some axioms yields
. Thus
and so
is an upper bound.
Then we must show that it is the least upper bound. Suppose it is not the least and let
equal to
which is positive by the assumptions. Now we have
and
for all
.
Let us show that then also
for some
. But now
. As an exercise, verify which axioms were used.

Remark
This
is what could be called an infinitely small number or an infinitesimal. The above essentially shows that Axioms 1–17 imply the non-existence of infinitesimals.

In the definition of 0.9999….. you are missing the symbol of natural number at least in two places :)
Thanks, corrected.