In Peano's Axioms are the uniqueness of the successor and the property $x^{\prime}=y^{\prime}\implies{x=y}$ redundant?
This seems obvious to me, but I may be missing something. In the various forms of the axioms used as the basis of natural number arithmetic that I have seen, the successor of a number is, in the axiom stating its existence, defined to be a unique number. That appears to require that $x^{\prime}=y^{\prime}\implies{x=y}$. So stating this result as an additional axiom is redundant.
On the other hand, $x^{\prime}=y^{\prime}\implies{x=y}$ seems insufficient to show that the successor of a number is unique.
From my perspective, such a redundancy is not particularly offensive if it aids in the applicability of the set of axioms. But such a feature should be explained, perhaps in a footnote. Since I have seen no such footnote, I am motivated to ask if others agree with my understanding.



NO.
We state that the successor relation $s(n)$ is defined by a function, in order to guarantee that there are no multiple values for the same argument.
But a function can map two arguments to the same value.
This is why we rquire that :
I.e., by contraposition, if the two arguments $n$ and $m$ are distinct, also their successors must be.
This is why Peano (1889) original formulation stated :
In the modern formulation in the language of first-order logic, the successor relation is expressed with a function symbol $s(n)$. Thus, the "functionality" is built-in into the rules of the language and thus the corresponding axiom amounts to :
This axioms is necessary to ensure the infinity of the number sequence; withou it, we may have some sort of "circularity", like e.g. $s(10)=2$. In this case, we have that both $1$ and $10$ have the same successor.