If we have a system of natural numbers that satisfies the Peano axioms (and we call the successor function s: N --> N) it seems to be standard to define the addition function as
f: N X N --> N such that
f(a, 0) = 0;
f(a, s(b)) = s(f(a, b)).
Now I intuitively understand how this definition works, but here's my question: since the definition is recursive, how can we know that it actually represents a unique function that provides an output for every input?
For example, we could define a recursive function where no output would be possible, because the "workings" of the function would never resolve themselves, e.g. f(x) := f(x) + 1.
How can we rigorously prove that the definition of addition isn't like that?