2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ What does the notation $a++$ mean? $\endgroup$ – Björn Friedrich Jul 13 '17 at 13:29
  • $\begingroup$ @BjörnFriedrich It means the increment or successor of a. $\endgroup$ – Phaedrus Zihan Jul 13 '17 at 13:31
  • 1
    $\begingroup$ 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. $\endgroup$ – Bettybel Jul 13 '17 at 13:31
  • 2
    $\begingroup$ 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$". $\endgroup$ – Mauro ALLEGRANZA Jul 13 '17 at 13:35
  • $\begingroup$ @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). $\endgroup$ – Mauro ALLEGRANZA Jul 13 '17 at 14:14
2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ This is incorrect. It is not any property of equality. It is a property of $f$. $\endgroup$ – Bettybel Jul 13 '17 at 13:51
  • $\begingroup$ @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. $\endgroup$ – Henning Makholm Jul 13 '17 at 13:59
  • $\begingroup$ So it is an axiom schema, right? $\endgroup$ – Phaedrus Zihan Jul 13 '17 at 14:24
  • $\begingroup$ @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. $\endgroup$ – Henning Makholm Jul 13 '17 at 17:15
0
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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{++}$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.