Proof of the standard algorithm for addition?

Can anyone present or point me toward a formal proof of the validity of the standard algorithm we all use for addition (line up your numbers one over the other, add the ones-place, carrying 'excess' digits to the next place-value, etc)?

This is what comes of reviewing set theory, elementary arithmetic, and proof theory at the same time :)

-
en.wikipedia.org/wiki/… It has parts for non-natural numbers as well. If you want to try it yourself, start by thinking of the binary numbers – mardat Mar 5 '13 at 23:09
I would maybe try to prove this by induction on the number of digits. – orlandpm Mar 5 '13 at 23:26
Relevant: (how base conversion works) cs.stackexchange.com/a/10495/7081 – user58512 Mar 12 '13 at 21:53

Notation To denote a string of digits I will use $\bar c$ and $\bar c d$ to denote a string of digits with a single digit $d$ at the end. e.g. maybe $\bar c = 84868786$ and $d = 2$ then $\bar c d = 848687862$, but it is important to note these are strings of digits and not natural numbers.

Induction We will use the following induction principle on pairs of nonempty strings of decimal digits:

Given a predicate $P$ defined on nonempty strings of digits, then if we prove

• for all digits $d,d'$, $P(d,d')$
• for all strings of digits $\bar c, \bar c'$, and digits $d, d'$, $P(\bar c, \bar c') \implies P(\bar c d, \bar c' d')$

we may deduce $P(\bar c, \bar c')$ holds for all pairs of nonempty strings of digits of the same length.

This induction principle is easily proved from the normal induction scheme for natural numbers.

Statement We want to prove the addition algorithm works by induction on the strings of digits, we will also need to worry about carries. Let us define the algorithm for addition of two strings (with a carry which will always be 0 or 1) of the same length as a function:

$$\begin{array}{rcl} \text{add}(k,d,d') &=& \text{carry}(k,d,d')\text{adder}(k,d,d') \\ \text{add}(k,\bar c d,\bar c' d') &=& \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')\text{adder}(k,d,d') \end{array}$$

I leave the definitions of $\text{carry}$ and $\text{adder}$ to the reader.

To say that the algorithm gives the same as true addition, we need to define an interpretation of strings of natural numbers:

We first define $[\![d]\!] = d$ mapping from digits (the set $\{0,1,2,3,4,5,6,7,8,9\}$) to natural numbers. Then we recursively define $[\![\bar c d]\!] = 10 \cdot [\![\bar c]\!] + d$. For example $[\![42]\!] = 10\cdot 4 + 2 = 42.$

So we may now define the predicate $$P(\bar s,\bar s') :\!\!\iff \forall k, [\![\text{add}(k,\bar s,\bar s')]\!] = k+[\![\bar s]\!]+[\![\bar s']\!]$$ which states that addition algorithm gives the same result as true addition for the strings $\bar s,\bar s'$ with any carry $k$.

Proof We prove by induction $\forall \bar s, \bar s', P(\bar s, \bar s')$.
base case: We must show that $$\begin{array}{rcl} \forall k \in \{0,1\}, && [\![\text{carry}(k,d,d')\text{adder}(k,d,d')]\!] \\ &=& 10 \cdot \text{carry}(k,d,d') + \text{adder}(k,d,d') \\ &=& k + d + d' \\ &=& k+[\![d]\!]+[\![d']\!] \end{array}$$

this can be done by trying all possible cases ($200$ of them), or slightly less directly using modular arithmetic. In any case $\text{carry}$ and $\text{adder}$ are defined to make this hold.

recursive step: We must show that forall $k \in \{0,1\}$, $$\begin{array}{rcl} && [\![ \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')\text{adder}(k,d,d') ]\!] \\ && 10 \cdot [\![ \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')]\!] + \text{adder}(k,d,d') \\ &=& 10 \cdot ([\![\bar c]\!]+[\![\bar c']\!]) + k + d + d' \\ &=& k+[\![\bar c d]\!]+[\![\bar c' d']\!] \end{array}$$

for this we will first re-use our base case to rewrite the problem as $$\begin{array}{rl} && 10 \cdot [\![ \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')]\!] + \text{adder}(k,d,d') \\ &=& 10 \cdot ([\![\bar c]\!]+[\![\bar c']\!]) + 10 \cdot \text{carry}(k,d,d') + \text{adder}(k,d,d') \end{array}$$

and from this drops out $$\begin{array}{rl} && [\![ \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')]\!] \\ &=& \text{carry}(k,d,d') + [\![\bar c]\!]+[\![\bar c']\!] \end{array}$$ which is immediate by our induction hypothesis.

From this we conclude that the addition algorithm is legitimate.

-
Wow, nice work. Is this the kind of thing one might cover in a group theory course, or maybe number theory? Or just set theory? Regardless, thanks for the rigorous proof! – ivan Mar 6 '13 at 0:04
@ivan, I can't imagine you would see anything like this anywhere else than here. – user58512 Mar 6 '13 at 0:05
It's surprising how long the proof is for such a simple algorithm... – user4205580 Feb 6 '15 at 21:51

If you know about polynomial arithmetic then integer addition is nothing but a special case of polynomial addition in $\rm\:\Bbb Z[x]/(x\!-\!b) =$ integer coefficient polynomials modulo $\rm\:x\!-\!b,\:$ where $\rm\:b\:$ is the radix. Indeed, mod $\rm\:x\!-\!b\:$ we can choose as a complete system of reps the polynomials whose coefficients lie in the interval $\rm[0,b\!-\!1]$. Then addition is simply polynomial addition, followed by the usual carry propagation to reduce the sum to normal form. This is an explicit constructive form of the isomorphism $\rm\:\Bbb Z \,\cong\, \Bbb Z[x]/(x\!-\!b)\:$ arising from the evaluation homomorphism $\rm\:f(x)\to f(b).$

For example, the computation $\ 298 + 97\, =\, 395\$ in radix $\,10\:$ is as follows

$\qquad\begin{eqnarray}\rm mod\ x\!-\!10\!:\,\ \,2x^2\!+\!9x\!+\!8\,+\, 9x\!+\!7\!\!\! &\ \equiv\ &\rm 2x^2+18x+15\\ &\equiv\, &\rm 2x^2+18x+(x\!+\!5)\\ &\equiv\, &\rm 2x^2+19x+5\\ &\equiv\, &\rm 2x^2+(x\!+\!9)x+5\\ &\equiv\,&\rm 3x^2+9x+5\\ \end{eqnarray}$

Above, carry propagation amounts to interpreting $\rm\:10\!+\!n\,\equiv\, x\!+\!10\:$ as a rewrite rule, in order to rewrite the polynomial to one in normal form, i.e. with all coefficients in the interval $\,[0,9].$

Remark $\$ For a more interesting example, see the following generalization for real numbers, where properly handling carry propagation is much trickier:  F. Faltin, N. Metropolis, B. Ross, G.-C. Rota, The real numbers as a wreath product. Advances in Math. 16 (1975), 278-304.

-
I still haven't tackled a full-on proof yet, but I've been working through a college algebra text and getting a good refresher on polynomial division. After much practice, I'm starting to get comfortable with it and see/understand why it all works. In comparison, the addition algorithm seems like cake. I'm still gonna do a proof though, once I finish this text and start some abstract algebra. – ivan Mar 13 '13 at 3:09