Is there a way to prove that $2+2$ really equals $4$?

There are many ways of defining $\mathbb{N}.$ In the context of this question, the details aren't that important; what matters is that $\mathbb{N}$ ends up being a set equipped with a distinguished function $S : \mathbb{N} \rightarrow \mathbb{N}$ and a distinguished element $0 \in \mathbb{N}$ subject to a theorem that says "definitions by recursion work." This allows us to prove the existence and uniqueness of a binary operation $+$ on $\mathbb{N}$ satisfying the following specifications. $$n+0 = n, \quad n+S(m) = S(n+m)$$

Now write $4$ as shorthand for $S(S(S(S(0))))$ and write $2$ as shorthand for $S(S(0)).$ Then we have

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

Extra Information.

For completeness, here's several ways of defining the naturals.

1. The algebraic structure $\mathbb{N}$ can be defined as the sole (up to unique isomorphism) model of the Peano Postulates (which are second order).

2. It can also be defined as the free monounary algebra generated by the singleton set $\{0\}$ (I suggest googling this term if you do not know it).

3. Set theorists like defining it as the least set $\omega$ such that firstly, $\emptyset \in \omega,$ and secondly, $x \in \omega$ implies $x \cup \{x\} \in \omega$. The entity $\emptyset$ ends up being our $0$, and the function $x \mapsto x \cup \{x\}$ ends up being our successor function.

The usual approach for formally proving that $2+2=4$ is to start from Peano's axioms (which define the set $N$ of natural numbers , $0\in N$ and a successor function on $N$). Using these axioms, along with the rules of logic and set theory, you can formally prove that there exists a unique binary function $+$ such that

$x+0 = x$

$x+(y+1) = (x+y)+1$

where $1$ is the successor of $0$, and $n+1$ is the successor of $n$.

This is a long and tedious process. (Earlier versions of Peano's axioms gave you the above definition to start.)

Then you define 2, 3 and 4 such that

$2=1+1$

$3=2+1$

$4=3+1$

Then you have $2+2=2+(1+1)=(2+1)+1=3+1=4$

We assume the Peano axioms. Specifically:

1. Zero is a number.
2. If a is a number, the successor of a is a number.
   (We denote the successor of $x$ as $x'$.)
3. Zero is not the successor of a number.
4. Two numbers of which the successors are equal are themselves equal.
5. (induction axiom.) If a set S of numbers contains zero and also the successor of every number in S, then every number is in S.

We then define addition recursively as follows:

$$a+0 = a$$ $$a+b' = (a+b)'$$

Now, we will name some numbers. We will denote:

$$\begin{align} 0' &= 1 \\ 1' &= 2 \\ 2' &= 3 \\ 3' &= 4 \end{align}$$

We could keep going, but we only need to be able to denote the numbers $0$ through $4$ (inclusive).

Now, showing that $2+2 = 4$ is a simple application of the recursive formula for addition: $$\begin{align} 2 + 2 &= 2 + 1' \\ &= (2+1)' \\ &= (2+0')' \\ &= ((2+0)')' \\ &= ((2)')' \\ &= 3'\\ &= 4 \end{align}$$