0.999999……=1? (continuation)

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.

[tex]0.999\ldots = 1[/tex].

Proof.

Let us review the axiomatization of the real numbers. The vocabulary is [tex]v=\{0,1,+,\cdot\}[/tex]. All axioms except one are first-order sentences over this vocabulary and one is second-order ([tex]\Pii[/tex] in fact). The symbols [tex]0[/tex] and [tex]1[/tex] are constants and [tex]+[/tex] and [tex]\cdot[/tex] 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 [tex]x[/tex] and [tex]y[/tex] there exists a unique number denoted by [tex]x+y[/tex], same for [tex]\cdot[/tex], and then list the following axioms. Constant symbols [tex]0[/tex] and [tex]1[/tex] are taken only for convenience since they are definable from [tex]+[/tex] and [tex]\cdot[/tex] 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: [tex]\forall x\forall y\forall z((x+y)+z=(x+(y+z)))[/tex]
Axiom 2: [tex]\forall x (x+0=0+x=x)[/tex]
Axiom 3: [tex]\forall x\exists y (x+y=y+x=0)[/tex]
Axiom 4: [tex]\forall x\forall y(x+y=y+x)[/tex]
Axiom 5: [tex]\forall x\forall y\forall z((x\cdot y)\cdot z=x\cdot(y\cdot z))[/tex]
Axiom 6: [tex]\forall x (x\cdot 1=1\cdot x=x)[/tex]
Axiom 7: [tex]\forall x\exists y (x\cdot y=y\cdot x=1)[/tex]
Axiom 8: [tex]\forall x\forall y(x\cdot y=y\cdot x)[/tex]
Axiom 9: [tex]\forall x\forall y\forall z(z\cdot(x+y)=z\cdot x+z\cdot y)[/tex]
Axiom 10: [tex]0 < 1[/tex]
Axiom 11: [tex]\forall x\forall y\forall z(x<y\land y<z\rightarrow x<z)[/tex]
Axiom 12: [tex]\forall x(\lnot (x<x))[/tex]
Axiom 13: [tex]\forall x\forall y((x<y)\lor (y<x)\lor (x=y))[/tex]
Axiom 14: [tex]\forall x\forall y\forall z((x+y)+z=(x+(y+z)))[/tex]
Axiom 15: [tex]\forall x\forall y\forall z(x<y\rightarrow x+z<y+z)[/tex]
Axiom 16: [tex]\forall x\forall y(x>0\land y>0\rightarrow x\cdot y>0)[/tex]
Axiom 17: Let [tex]R[/tex] be a unary second order variable. The completeness axiom states:

[tex]\forall R\big[\exists x\in R\rightarrow [/tex]
[tex]\big[\exists x\big(\forall y(R(y)\rightarrow x>y)\big)\rightarrow [/tex]
[tex] \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].[/tex]

In words, all non-empty subsets [tex]R[/tex] 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 [tex]A[/tex] be a set with an upper bound. Then there exists a unique [tex]x[/tex] which is the least upper bound.

Proof of Claim 1
Suppose [tex]x[/tex] and [tex]y[/tex] are two upper bounds:

[tex]\forall z_0\in A\,(z_0<x)\land \forall z_1<x\exists z_2\in A(z_1<z_2<x)\eqno (*)[/tex]

[tex]\forall z_0\in A\,(z_0<y)\land \forall z_1<y\exists z_2\in A(z_1<z_2<y)\eqno(**)[/tex]

If we show that neither [tex]y<x[/tex] nor [tex]x<y[/tex] holds, then by axiom 13 it will follow that [tex]x=y[/tex]. Suppose that [tex]y<x[/tex]. Then substituting [tex]y[/tex] in place of [tex]z_1[/tex] we get as a consequence

[tex]\exists z_2\in A(y<z_2)[/tex]

which implies that [tex]y[/tex] is not an upper bound which is a contradiction. Similarly if [tex]x<y[/tex], then by substituting [tex]x[/tex] in place of [tex]z_1[/tex] in [tex](**)[/tex] we get that [tex]x[/tex] is not an upper bound which is a contradiction again.

To proceed, we must define [tex]0.999\ldots[/tex]. I choose to define it in the following way which is equivalent to all conventional ways:
Definition
[tex]0.999\dots[/tex] is the unique least upper bound of the set

[tex]B=\{(10^n-1)\cdot (10^n)^{-1}\mid n\in \mathbb{N}\}[/tex]

where: [tex]\mathbb{N}[/tex] is the set of natural numbers, [tex]10=1+1+1+1+1+1+1+1+1+1[/tex], the operation [tex]x\mapsto x^k[/tex] is recursively definable by [tex]x^0=1[/tex] and [tex]x^{n+1}=x^n\cdot x[/tex] and the operation [tex]x\mapsto x^{-1}[/tex] 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 [tex]\mathbb{N}[/tex]. It can be justified as follows. First, if we assume the non-existence of [tex]\mathbb{N}[/tex], 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 [tex]0.999\ldots[/tex] which, to put it mildly, is hard to maintain without the existence of [tex]\mathbb{N}[/tex].

Once we prove that [tex]1[/tex] is a smallest upper bound for the set [tex]B[/tex], Claim 1 implies that [tex]0.999\ldots=1[/tex]. In order to prove that, we need to show that the sentence [tex](*)[/tex] in the beginning of the proof with [tex]A[/tex] replaced by [tex]B[/tex] and [tex]x[/tex] replaced by [tex]1[/tex] holds. Suppose [tex]z_0\in B[/tex]. Then for some [tex]n[/tex], [tex]z_0=(10^n-1)\cdot (10^n)^{-1}[/tex]. By axioms 4, 10 and 15, [tex]10^n<10^n+1[/tex] which implies [tex]10^n-1<10^n[/tex], where subtraction is the addition of the additive inverse whose existence follows from axiom 3. By the same axioms we get [tex]0<10^n-(10^n-1)[/tex]. Multiplying both sides by [tex](10^n)^{-1}[/tex] and applying axiom 9 we get [tex]0<1-(10^n-1)\cdot (10^n)^{-1}[/tex] which, after applying some axioms yields [tex](10^n-1)\cdot (10^n)^{-1}<1[/tex]. Thus [tex]z_0<1[/tex] and so [tex]1[/tex] is an upper bound.

Then we must show that it is the least upper bound. Suppose it is not the least and let [tex]c[/tex] equal to [tex]1-0.999\ldots[/tex] which is positive by the assumptions. Now we have [tex]1-c=0.999\ldots[/tex] and [tex]c<(10^n)^{-1}[/tex] for all [tex]n[/tex].

Let us show that then also [tex]c+c(10^n)^{-1}[/tex] for some [tex]n[/tex]. But now [tex]c=(c+c)\cdot 2^{-1}=2^{-1}\cdot (10^n)^{-1}>10^{-1}\cdot (10^n)^{-1}=(10^{n+1})^{-1}[/tex]. As an exercise, verify which axioms were used.
[tex]\square[/tex]

Remark
This [tex]c[/tex] 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.