How do you formally define the addition algorithm for the natural numbers and then prove it? I am interested in knowing what a set theoretic definition of the standard addition algorithm for the natural numbers would be. Second, how do we know the standard algorithm gives the correct sum? Is there a gold standard for addition that we could compare it to?
It seems if you have two disjoint sets and you want to add the elements of one set to the other, you would just add one element to the receiving set and subtract one from the giving set and repeat this until the giving set is empty. Then you would just count the number of elements in the receiving set and that would be the sum. To me this would be the gold standard, but I’m not sure.
If you forget everything you know about addition and try to create a faster method of adding than the procedure above, the standard algorithm doesn’t seem very obvious to me.
Lastly, are there any writings about this topic that someone could direct me to? This is so basic and uninteresting to most people that I couldn’t find much on the topic.
I have seen one answer on here that defines the algorithm and proves it, but it was so hard to follow and I don’t think it was compared to any gold standard to make sure we get the correct answer.
I really need it dumbed down for me. It’s been awhile since I have been in school. Thank you.
 A: Your procedure for "adding" two numbers is a fine algorithm if implemented correctly, however, it does not constitute a true additive function $\omega\times\omega\to\omega$ without making your procedure more precise.
The following theorem is hopefully an easily accessible proof of the existence and uniqueness of the addition function on the natural numbers.
Some Preliminaries:
Definition: $\omega$ is the set of natural numbers, defined to be the smallest inductive set (see the axiom of infinity or any intro to set theory article for more on how to construct $\omega$).
Definition: A relation $f\subseteq X\times Y$ is a function from $X$ to $Y$ provided that $\forall x\in X\exists!y\in Y:(x,y)\in f$. The unique $y$ corresponding to each $x$ is denoted $f(x)$.
Successor Function: There exists a function $s:\omega\to\omega$. Take $s=\{(x,y)\in\omega\times\omega:y = x\cup\{x\}\}$ and show that this is indeed a function with $s(x)=x\cup \{x\}$ (this encapsulates the idea of adding one to $x$).
I assume you have knowledge of the principle of induction and how to follow an inductive proof.

Theorem: There exists a unique function $+:\omega\times\omega\to\omega$ satisfying
$$\forall x\in\omega:x+0 = x\tag{i}$$
$$\text{ and }$$
$$\forall x,y\in\omega:x+s(y) = s(x+y)\tag{ii}$$

Proof:
Call a subset $A$ of $\omega^3$ additive if
$$\forall x\in\omega:(x,0,x)\in A\tag{a}$$
$$\text{and}$$
$$\forall x,y,z\in\omega:(x,y,z)\in A\implies (x,s(y),s(z))\in A\tag{b}$$
Note that this definition is not so restrictive that no subset of $\omega^3$ satifies these conditions, since trivially, $\omega^3$ is additive.
Set $$\mathcal{A}=\{A\in\mathcal{P}(\omega^3):A\text{ is additive }\}$$ and define $+=\bigcap\mathcal{A}$. Our current goal is to show that $+$ is additive (that is, $+$ satisfies (a) and (b)) and that $+$ is a function.
(a) For $x\in\omega$, $(x,0,x)\in A$ for all $A\in\mathcal{A}$ hence $(x,0,x)\in +$.
(b) For $x,y,z\in\omega$, if $(x,y,z)\in +$, then $(x,y,z)\in A$ for all $A\in\mathcal{A}$, hence $(x,s(y),s(z))\in A$ for all $A\in\mathcal{A}$, thus $(x,s(y),s(z))\in+$.
Since $+$ satisfies (a) and (b), then $+$ is additive and is the smallest additive subset of $\omega^3$.
We now show that $+$ is a function via induction. Fix $x\in\omega$ and define
$$N_x=\{y\in\omega:\exists!z\in\omega:(x,y,z)\in +\}$$
I leave it to you to show that $0\in N_x$. Now suppose that $y\in N_x$ for some $y\in\omega$. Then there exists a unique $z\in\omega$ such that $(x,y,z)\in+$. As $+$ is additive, then $(x,s(y),s(z))\in+$. If $z'\in\omega$ satisfies $(x,s(y),z')\in +$, then $+\setminus\{(x,s(y),z')\}$ is an additive subset, contradicting minimality of $+$, hence $s(y)\in N_x$. This completes the induction.
It now follows that for all $(x,y)\in\omega\times\omega\exists!z\in\omega:(x,y,z)\in+$, that is, $+$ is a function from $\omega\times\omega$ to $\omega$.
It is clear that $+$ is unique since any other function satisfying (i) and (ii) must be an additive subset of $\omega^3$. You may also check that $+$ indeed satisfies (i) and (ii). $\square$
Properties (i) and (ii) uniquely characterize addition on the natural numbers in the way we are all familiar with, and we have simply constructed a function from the ground up which satisfies the characteristic properties of addition on the natural numbers. This gives you an algorithm to add any two natural numbers based in standard set theory by recursively applying the successor function and the relations $+$ satisfies .
