Verification: Is it the theorem to we need to define the predecessor a natural number?

Question

Define the predecessor of a natural number $n$ as: $\vdash 0^− = 0 $

$\vdash (∀n)((n^+)^− = n)$

Consider to get a theory by adding this function symbol. As the way discribed in this picture

We need a theorem in the form $\vdash (∀x_1)(∀x_2)...(∀x_n)(∃!u)P(u,x_1,x_2,...,x_n) $ to add the function symbol of predecessor.

May I please ask is there this theorem $\vdash (∀x_1)(∀x_2)...(∀x_n)(∃!u)P(u,x_1,x_2,...,x_n) $ is just $\vdash (∀x)(∃!u)(u^+=x) $?

Thanks in advance!

Answer 1

Your formula $P(u,x) : (\forall x)(\exists!u)(u^+=x) $ has an immediate problem for $x = 0$, because that would mean that there is a (unique) $u$ such that $u^+ = 0$, but that goes against Peano Axiom 1 (I assume you are working within the Peano Axioms ... indeed I assume the text you provided refers to the Peano axioms with their PL1-PL6)

So you need to treat $x = 0$ as a special case. So, how about:

$P(u,x) : (x = 0 \land u = 0) \lor (x = u^+)$