Every rational number has an infinite repeating decimal expansion. In particular, every integer admits two decimal expansions: one with and one without a "tail of nines". This means that 1 = 0.9999…, a provable fact that many people still choose to disbelieve. What do I mean here by "provable"? I mean "provable by finitistic reasoning", that is, by a purely algebraic proof free of notions of continuity or convergence. The proof in this particular (and particularly popular) case goes like this:

x = 0.9999… ≡ { product by base is shift of decimal point } 10x = 9.9999… ≡ { subtraction of finitely-expanded integer } 10x - 9 = 0.9999… ≡ { identity of decimal expansion } 10x - 9 = x ≡ { algebra } 9x = 9 ≡ { cancellation of multiplication } x = 1

The last two steps are elementary consequences of the fact that integers form a ring. The first three steps require justification. By definition, a decimal expansion of a positive real number `x` is a (possibly semi-infinite) sequence of digits 0 ≤ `d _{i}` < 10 such that for all

`i`≥

`N`,

`d`= 0, and

_{i}x= ⟨∑i:: 10^{i}⋅d⟩_{i}

and the decimal point separates the digits corresponding to 10^{0} and 10^{-1}, namely `d _{0}` from

`d`.

_{-1}

Lemma 0Any decimal numberxcan be expressed as the sum of an integer and a (possibly infinite) decimal part

Proof:By definition,xhas a finite number of decimal digits to the left of the decimal point, namely for 0 ≤i<N, hence:x= { definition } ⟨∑i:: 10^{i}⋅d⟩ = { associativity of addition, a_{i}finitenumberNof times } ⟨∑i: 0 ≤i<N: 10^{i}⋅d⟩ + ⟨∑_{i}i: 0 >i: 10^{i}⋅d⟩ = { naming the first term }_{i}n+ ⟨∑i: 0 >i: 10^{i}⋅d⟩_{i}

This justifies representing a positive real number as a pair of an integer and a possibly infinite purely fractional decimal expansion:

type dec = Dec of int * int list

A sufficient condition for two numbers to be equal is that their decimal representations are the same:

let eq (Dec (e, ds)) (Dec (e', ds')) = e = e' && ds == ds'

Here, since the decimal expansions could be infinite, I use physical equality on lists. This is a stronger condition than stated above. Now, the proof for the first step:

Lemma 1Multiplying a positive real numberxby 10 shifts the decimal point in its decimal expansion one place to the right

Proof:10⋅x= { lemma 0 } 10⋅(n+ ⟨∑i: 0 >i: 10^{i}⋅d⟩) = { product finitely distributes over sum } 10⋅_{i}n+ 10⋅⟨∑i: 0 >i: 10^{i}⋅d⟩ = { product formally distributes over sum } 10⋅_{i}n+ ⟨∑i: 0 >i: 10^{i+1}⋅d⟩ = { substitute_{i}i:=i-1 } 10⋅n+ ⟨∑i: 1 >i: 10^{i}⋅d⟩ = { lemma 0 } (10⋅_{i-1}n+d) + ⟨∑_{0}i: 0 >i: 10^{i}⋅d⟩_{i-1}

Note that the third step is not strictly speaking finitist but formal: it requires taking the distributivity of product over a summation as axiomatic if induction is not accepted. This justifies the following:

let mul10 = function | Dec (e, [] ) -> Dec (10 * e , []) | Dec (e, d :: ds) -> Dec (10 * e + d, ds)

The proof for the second step:

Lemma 2Subtracting an integerkfrom a positive real numberxonly affects its integer part

Proof:x-k= { lemma 0 } (n+ ⟨∑i: 0 >i: 10^{i}⋅d⟩) -_{i}k= { commutativity and associativity of sum } (n-k) + ⟨∑i: 0 >i: 10^{i}⋅d⟩_{i}

This justifies the following:

let subi (Dec (e, ds)) n = if e < n then failwith "subi" else Dec (e - n, ds)

Now the proof for the third step is purely executable and relies on physical equality of infinite lists of digits represented as circular lists:

let nines = let rec ds = 9 :: ds in Dec (0, ds)

Of course, for more general repeating expansions, equality on heads won't suffice, but this case is nicely handled by a one-liner:

let lemma = assert (eq nines (subi (mul10 nines) 9))

The purely verbal mathematical statement of this truth is that, since the first two steps operate on a finite prefix of the infinite expansion, the inifinite suffix is unchanged by the operations and hence identical to itself. In other words, the infinite summation is a purely formal object that remains unchanged from step to step.

Will this proof finally lay the "controversy" to rest, persuading even the staunchest finitist?

*Edit:* Thanks to id that alerted me in my confusion between structural and physical equality.

## 2 comments:

Actually here physical equality is tested, as structural comparison will not terminate.

@id: thank you for the heads-up. I've corrected the article.

Post a Comment