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 🙂
Best Answer
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
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.