Prove that $4$ is the only solution to $2+2$. [duplicate]

This question was featured on Saturday Morning Breakfast Cereal and I haven't been able to find a proof. Can anyone help?

When proving theorems in mathematics, one starts from a set of axioms, statements that are accepted as true without argument. You might ask, "but what if an axiom isn't true?", and the answer is that we would be dealing with different mathematics. For example, Euclid included the parallel postulate as an axiom in his elements. For years mathematicians tried to prove that the parallel postulate could be derived from the other axioms. It turns out that if you don't accept the parallel postulate, you end up with different types of geometry that we now call non-euclidean. Einsteins theory of general relativity depends on these geometries.

To come up with a proof of such a seemingly simple fact as $2 + 2 = 4$, we need a set of axioms to start with, and we need precise definitions of all the terms we are using. Depending on what set of axioms you start with, proving that $2 + 2 = 4$, and that no other natural number can equal $2+2$ may be either very simple or surprisingly difficult. For example in Russell and Whitehead's Principia, it famously took over 300 pages of work before they could prove that $1+1=2$. They started with a very sparse set of axioms though.

The most common set of axioms for the natural numbers are the Peano Axioms.

They are

1. $0$ is a natural number.
2. For every natural number $x$, $x=x$.
3. For all natural numbers $x$ and $y$, if $x = y$, then $y = x$.
4. For all natural numbers $x$, $y$, and $z$, if $x = y$ and $y = z$, then $x = z$.
5. For all $a$ and $b$, if $a$ is a natural number, and $a = b$, then $b$ is a natural number.
6. For every natural number $n$, $S(n)$ is a natural number.
7. For every natural number $n$, $S(n) = 0$ is false.
8. For all natural numbers $m$ and $n$, if $S(m) = S(n)$ then $m = n$.
9. If $K$ is a set such that $0 \in K$, and for every natural number $n$, $n \in K$ implies that $S(n) \in K$, then $K$ contains all natural numbers.

Here $S$ is the successor function, it takes each natural number to its successor. This might seem like a complicated mess compared to the simplicity of natural numbers, but we need to be precise. We need to carefully construct the axioms so that no contradiction can be derived from them, and so they encapsulate what we understand to be the natural numbers. We want to be able to prove interesting statements about the natural numbers from them. Note that the axioms contain undefined terms. The axioms don't need to state what the terms mean, only what they do.

The following definitions are commonly used within this axiomatization. They are the definitions from Peano's original paper (An English translation is available in the book From Frege to Gödel), modified to start at $0$ instead of $1$.

$1$ is defined as $S(0)$, $2$ is defined as $S(1)$, $3$ is defined as $S(2)$, and $4$ is defined as $S(3)$. Addition is defined recursively as follows.

$$a + 0 = a$$ $$a + S(b) = S(a + b)$$.

Thus

$$2 + 2 = 2 + S(1) = S(2 + 1) = S(2 + S(0)) = S(S(2 + 0)) = S(S(2)) = S(3) = 4$$

proving that $2+2 = 4$.

This is the unique value of $2+2$ by axiom 4.

If $x = 2+2$ and $2+2 = 4$, then $x = 4$.

From the Peano axioms.

First recall that $2$ is really a shorthand for $S(S(0))$ and $4$ is a shorthand for $S(S(S(S(0))))$. Now we have the axioms for addition, $x+0=x$ and $x+S(y)=S(x+y)$. We calculate:

$$2+2=S(S(0))+S(S(0))=S(S(S(0))+S(0))=S(S(S(S(0))+0))=S(S(S(S(0)))=4$$

To prove uniqueness we use the axioms that $0\neq S(x)$, $x\neq0\rightarrow \exists y(x=S(y))$ and $S(x)=S(y)\rightarrow x=y$:

$$S(S(S(S(0))))=S(S(0))+S(S(0))=x\implies\exists y(x=S(y))\implies S(S(S(0))=y\implies\exists z(S(z)=y)\implies z=S(S(0))=2$$

Therefore $z=2$ and so $y=3$ and $x=4$ as wanted.