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

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?

• What does the notation $a++$ mean? – Björn Friedrich Jul 13 '17 at 13:29
• @BjörnFriedrich It means the increment or successor of a. – Phaedrus Zihan Jul 13 '17 at 13:31
• That property is a consequence of $++$ being an operation, in particular a function. If you want, that is part of his Axiom 2.2, which is written a bit succinctly. – Bettybel Jul 13 '17 at 13:31
• The successor function is a function; thus, by def, if $a=b$, then $succ(a)=succ(b)$. See page 16: "Thus, to define the natural numbers, we will use two fundamental concepts: the zero number $0$, and the increment operation. In deference to modern computer languages, we will use $n++$ to denote the increment or successor of $n$". – Mauro ALLEGRANZA Jul 13 '17 at 13:35
• @Bettybel - NO, it is not part of Ax.2.2 that is right as is. It is part of the language used (see page 16). – Mauro ALLEGRANZA Jul 13 '17 at 14:14

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.
• This is incorrect. It is not any property of equality. It is a property of $f$. – Bettybel Jul 13 '17 at 13:51
• @Bettybel: It is a fundamental property of equality that $t_1=t_2$ implies $t_3[x\mapsto t_1] = t_3[x\mapsto t_2]$ for all $t_1$, $t_2$, $t_3$. This is built into first-order logic -- or semantically: it is impossible for any first-order structure not to satisfy this. – Henning Makholm Jul 13 '17 at 13:59
• @PhaedrusZihan: It can be -- but that depends on the precise details of how your proof system is set up. It can also be an inference rule -- or one might specificy, for example, that each function symbol $f$ implicitly generates a bunch of logical axioms of the form $y_1=y_2 \to f(x,y_1,z)=f(x,y_2,z)$ and each predicate symbol $p$ comes with axioms of the form $y_1=y_2 \to p(x,y_1,z) \to p(x,y_2,z)$. Then you would use the usual first-order machinery to derive instances of the above rule piece for piece. – Henning Makholm Jul 13 '17 at 17:15
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.
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{++}$.