1. ## Help with recursive definition of addition

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?

2. Nevermind, I managed to figure out a way. I used the "induction" Peano axiom on the proposition "n provides an output when the recursive method is used on it". It's true for 0, and you can show that if it's true for n then it's true for s(n).