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 :)
 A: 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.
A: 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.
