The first question we should be asking ourselves is: What does 2+2=4 actually mean? What is 2? What is 4? What is +? And what is =? More generally, what is a Natural Number? And how are operations and relations defined over them?

Equality

You probably already know this, but I have to state it anyway. My answer needs to be logically closed (just be thankful I didn’t start from ZFC axioms, but whatever…). Anyway, equality is a relation between two things. Sure, but what is a relation?

A binary relation R between sets A and B is defined as follows:

R⊆A×B

Where × is the cartesian product. So aRb is true if and only if (a,b)∈R.

Equality = is a relation with the following properties:

Reflexivity: ∀x:x=x
Symmetry: ∀x,y:x=y⟹y=x
Transitivity: ∀x,y,z:((x=y∧y=z)⟹x=z)
Natural Numbers: The most beautifully unnatural thing ever

If you ask someone what is a Natural Number, you will usually hear “1,2,3,…” as if that settled the matter. The actual definition removes the ambiguity and makes the matter a lot more attractive. So, what are Natural Numbers?

The(∗) set N whose elements proves to respect the Peano Axioms is the set of Natural Numbers. Equality is defined over this set, meaning the Natural Numbers are closed under equality (obviously). Here are the Peano Axioms:

0∈N
The successor function S:N→N has the following properties:
∀n∈N:S(n)∈N
∀n,m∈N:m=n⟺S(n)=S(m)
∄n∈N:S(n)=0
Are we done? Well, let’s see what these axioms imply. The first thing we are told is that 0 is a Natural Number. By axiom 2a, S(0) is also in N. So is S(S(0)), S(S(S(0))) and S(S(…S(S(0)))). This looks like some kind of “line structure”, as if the set would admit a total order. But what if ∃n∈N,n≠0:(∄m∈N:S(m)=n)? That is, could there be a Natural Number that is not the successor of any Natural Number? Let’s see. Take the set:

M={0,S(0),S(S(0)),...,z,S(z),S(S(z)),...}

That is, the set including 0 and all of its successors and z and all of its successors. It has the aforementioned property that z is not the successor of any other Natural Number. Does M verify the axioms? Well, axiom 1 is trivially verified by looking at it. Axiom 2a is also verified: by how we defined the set, it turns out to be closed under the successor function. Similarly, 2b and 2c are also true of M. The set I constructed above has two totally independent “lines” (call them the 0 line and the z line) and therefore does not allow for a total order.

But…but…this isn’t what we want.

Natural Numbers arose as an intuitive way to understand some aspects of reality first, and it wasn’t until much, much later that the definition was captured formally. And we already had the intuitive grasp of how they should behave. In order to avoid M, we require an additional axiom.

Axiom of Induction: (0∈X∧(∀n∈N:n∈X⟹S(n)∈X)⟹N⊆X
This implies that every Natural Number, except 0, is the successor of another Natural Number. With the axiom of induction, a total (or sometimes called linear) order can be induced in N. Since it isn’t of much relevance in this answer, we won’t formally define the notion of total order.

Most readers who got to this point can see 2=S(S(0)) and 4=S(S(S(S(0)))), but in order to attain to mathematical formalisms, how can we construct N purely from set theoretic notions?

The Von Neumann Construction of the Natural Numbers

I’ll show how such feat can be accomplished. Define 0={} and S(n)=n∪{n}. Then:

S(0)={{}}

S(S(0))={{},{{}}}

S(S(S(0)))={{},{{}},{{},{{}}}}

(…)

I hope I didn’t miss anything in there, that’s pretty confusing in La. Anyhow, the idea is that the successor of n will contain every previous Natural Number, including n. It is easier to see that if we write it like this:

0={}

1=S(0)={0}

2=S(S(0))={0,1}

3=S(S(S(0)))={0,1,2}

(…)

As you can see, there are many sets which comply with the Peano Axioms, which we call “representations” or models of the abstract object N. That is, the sets are defined by different means, but semantically, they are exactly the same.

Enough with Natural Numbers themselves. Let’s go to the only thing left undefined: +

Addition on the Natural Numbers

Define an operation + over N as:

∀n∈N:n+0=n

∀a,b∈N:S(a+b)=a+S(b)

Sure enough, that implies that S(n)=n+1, since n+1=n+S(0) and by definition n+S(0)=S(n+0)=S(n). Is + associative and commutative as we would expect? Of course! And, as if that wasn’t enough beauty, we will use the Axiom of Induction. First, we need to know if ∀n∈N:0+n=n:

0 is the additive identity:
Define the predicate P(n) as ∀n∈N:0+n=n. P(0) clearly holds: 0+0=0 by the first definition. By the Axiom of Induction:

n+0=0+n⟹

S(n+0)=S(0+n)⟹

S(n)=0+S(n)⟹

∀n∈N:0+n=n

Associativity:
Define P(c) as ∀a,b∈N:(a+b)+c=a+(b+c)

P(0):

(a+b)+0=a+b

a+(b+0)=a+b

Now we have to show that:

P(c)⟹P(S(c)):

Assume P(c):

(a+b)+c=a+(b+c)⟹

S((a+b)+c)=S(a+(b+c))⟹

(a+b)+S(c)=a+S(b+c)⟹

(a+b)+S(c)=a+(b+S(c))

Commutativity:
Give the name P(ℓ) (ℓ∈N) to the predicate ∀n∈N:n+ℓ=ℓ+n. For ℓ=1:

P(1):

We will use 1 (since we’ve already shown 0 commutes with everything) as the base case and prove P(1) with induction over G(a):a+1=1+a. G(0) is of course trivial. Now let’s prove G(a)⟹G(a+1).

S(a)+1=S(a)+S(0)⟹

S(a)+1=S(S(a)+0)⟹

S(a)+1=S(a+1)⟹

By the induction hypothesis:

S(a)+1=S(1+a)⟹

S(a)+1=1+S(a)

The base case is done, inductive step to go!

P(ℓ)⟹P(S(ℓ)):

Assume P(ℓ):

n+ℓ=ℓ+n⟹

S(n+ℓ)=S(ℓ+n)⟹

n+S(ℓ)=ℓ+S(n)⟹

n+ℓ+1=ℓ+n+1

By the base case (1 commutes with everything):

n+ℓ+1=ℓ+1+n

n+S(ℓ)=S(ℓ)+n

And we’ve proven our favorite properties of addition directly from the definition!

The Actual Question

Now, I’ll prove 2+2=4. It’s a bit boring, but hopefully the way was somehow enlightening. Anyhow, 2=S(S(0)) and 4=S(S(S(S(0)))).

2+2=S(S(0))+S(S(0))⟹

2+2=S(S(S(0))+S(0))⟹

2+2=S(S(S(0))+1)⟹

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