I first met the Peano axioms many years ago in Landau's book Foundations of Analysis -- I still believe this is about the best development of the reals from the Peano axioms. I remember a little problem glossed over by Landau. Namely recursive definition. Landau defines addition exactly as you do in your post.
I think one needs a theorem that validates the recursive definition.
Theorem. Let X be a set, and . Then there exists a unique function such that g(0)=x and
The proof of uniqueness is trivial from the induction axiom, but the existence proof requires proving the intersection of all subsets T of with the property is such a function g. This last statement is straight forward using the axioms.