Is "if $a = b$ then $a{++} = b{++}$" an axiom or a lemma can be proved?

Question

I am currently learning Analysis I by Terence Tao. In his book Axiom 2.4:

Different natural numbers must have different successors; i.e., if $n, m$ are natural numbers and $n \neq m$, then $n{++} \neq m{++}$. Equivalently, if $n{++} = m{++}$, then we must have $n = m$.

We can't deduce "if $a = b$ then $a{++} = b{++}$" from this Axiom directly, so this question appears.

Suppose we use the Peano Axioms to define the natural numbers. Is "if $a = b$ then $a{++} = b{++}$" an axiom or a lemma can be proved? If it is a lemma, how to prove it from axioms?

Answer 1

From $a=b$ we can conclude $f(a)=f(b)$ for all $a, b$ and functions $f$ -- that does not need any axioms at all. This is part of how equality works in the first place, and will usually come as a built-in rule of first-order logic before you start writing down specific axioms of a theory.

This is in particular true when $f$ is the successor function.

Answer 2

The successor is uniquely defined. If $a$ is a natural number, there is one and only one natural number $c$ satisfying $a{++} = c$. Thus if $a = b$, $a$ and $b$ are the same number, their successors are the same number too, i.e., $a{++} = b{++}$.

Answer 3

Your question is really asking if the ${++}$ (successor) operation is well-defined. For an operation to be well-defined, it must return equal outputs for equal inputs, which is the exact same thing as saying $a = b$ implies $a{++} = b{++}$. By whatever axioms you've defined the successor operation, the operation should be well-defined.