Is there a way to prove that the addition of two natural numbers always gives the same value, i.e. $\forall a\forall b\exists!c(a+b=c)$?

Question

Natural numbers and addition are defined as per the Peano Axioms.

Edit:

To clarify my question, I have already proved that $\forall a\forall b \exists c:a+b=c$. I have trouble proving the second part, that $\forall a,b,c,d(a+b=c \land a+b=d \implies a+b=d)$.

The reason why I thought of this question is because I was thinking of square root, where IF we define the square root as $\sqrt a=b \iff a=b^2$, so we do NOT specify that $b$ must be pozitive. In this case $\sqrt a=b \land \sqrt a=c$ does NOT imply that $b=c$.

Answer 1

The reason why I thought of this question is because I was thinking of square root, where IF we define the square root as a−−√=b⟺a=b2, so we do NOT specify that b must be pozitive. In this case a−−√=b∧a−−√=c does NOT imply that b=c.

Yes. $a\to b$ so that $a = b^2$ is not injectively (uniquely) defined. But $a \to s(a) = a+1$ is (by axiom) injective.

$x + n$ is defined by induction. $x + 0 = x$ and $x + s(n) = s(x+n)$. As $x$ is presumed to be a unique natural number then $x + 0=x$ is a unique natural number for all natural $x$ and $0$.

If we assume we have defined $x + n$ to exists, and be unique, for all $x$ and that one specific value of $n$ then we can state that $x + s(n) = s(x+n)$ and as $s$ is injective, we know $x + s(n)$ is also a unique natural number. So $x + s(n)$ is a unique natural number for all natural $x$ and for $n$ and $s(n)$

And thus by induction $x +y$ is a unique natural number for all $x$ and any natural $y$.

Answer 2

For any non-zero real number $a$ there is no real number $b$ such that $\sqrt{a} = b \iff a = b^2$, therefore your putative definition of $\sqrt{}$ does not in fact define $\sqrt{}$.

More fundamentally, a function symbol (such as $+$ or $\sqrt{}$) is always assumed to have a single output for a given input in standard first-order logic. In other words, first-order logic simply does not allow you to work with "functions" whose output is not uniquely determined. Such objects are not functions from the perspective of first-order logic, they are relations. So there is, in fact, nothing to prove: in the language of Peano Arithmetic, $+$ is a function symbol, and that's all that needs to be said about the matter.