In Peano's Axioms are the uniqueness of the successor and $x^{\prime}=y^{\prime}\implies{x=y}$ redundant? 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.
 A: 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 :

$\text { if } s(n)=s(m), \text { then } n=m$.

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 :

$\text { for all natural numbers  } m \text {  and  } n  ( m = n \text {  if and only if  } s(m) = s(n))$.

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 :

$\text { for every  } n, m (\text {  if  } s(n) = s(m), \text {  then  } n=m )$.


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.
A: This is not redundat. Consider only the sentence $\phi\equiv\forall x\exists !y(y=S(x))$. Where $S$ is the succesor function. Now, consider the structure $\mathfrak{A}:=(M,S)$ where $M=\{0,1,2\}$, $S(i)=i+1$ if $i<2$ and $S(2)=2$. Here you see that $\mathfrak{A}\models\phi$ but $\mathfrak{A}\models\exists x, y(S(x)=S(y)\wedge x\neq y)$.
A: Let's say that S is the relation   : the natural number y is a successor of the natural number x. That is to say , the relation S is a subset of the cartesian product " N cross N" such that: 
S = { (x,y) | the nat.number y is a successor of the nat. number x } 
Remark. Here I say " a successor" since S being only defined at this stage as a relation, nothing prevents a natural number x to have more that more than one successor. Things will change at the next stage. 
The fact that the relation S is furthermore defined as a function guarantees that (1) each natural number has a successor and (2) not more than 1: briefly it guarantees each natural number has a unique successor. 
Adding to this that " S(x) is equal to  S(y)" implies that " x is equal to y" ( by contraposition, that " x is different from y" implies that " S(x) is different from S(y) " ) guarantees that no two different natural numbers have the same successor, in other words it guarantees that each natural number has its own/ proper successor . It means technically that the successor function is " one-one" ( injective). 
Let us notice that although the function S from N to N is injective ( one-one) it is not surjective ( " onto"). This is because the natural number 0 is not the image of any natural number under the function S : there is no natural number x such that S(x) = 0 
A: Visually, the successor relation on $N$ (from Peano's Axioms) should look like this:

We don't want anything like this:

Every number must be mapped to a unique successor. So, we require that the successor relation be a function.
We also don't want anything like this:

The predecessor of any number, if it exists, must also be unique. So, we require that the successor function be injective (to answer your question).
More on this topic at my blog posting here.
