Sorry if this question sounds a little bit stupid ; I've always had problems with "logical" concepts (implications, "if and only if" statements, quantifiers, etc.) and I've decided to tackle these problems once and for all, but I'm still having issues about some things.
Considering the Peano axioms, one of the axioms seems to be (it comes from here):
Two numbers of which the successors are equal are themselves equal.
But the same axiom of the Wikipedia article on Peano axioms seems to be
For all natural numbers $m$ and $n$, $m = n$ if and only if $S(m) = S(n)$. That is, S is an injection.
For some reason, the "if and only if" is really bothering me ; Wikipedia is the only place I found where the axiom is formulated that way, so I wondered if there were any example of a situation in which we could not have $n=m \Rightarrow n{++} = m{++}$, thus justifying the usual way this axiom is formulated (i.e. the first one I quoted). Except if such an example exists, I don't really understand why this axiom is not formulated everywhere as it is on Wikipedia, as it actually seems more "logical" to me (but, again, I'm not very logical. Always had issues with that sort of things). I'm pretty sure I'm just missing something here, but I don't know what it is, so any help is welcome! Thanks in advance.
In logic systems where equality is treated as a basic logical concept, one of its fundamental properties is that $m=n$ implies that $t_1=t_2$ when the only difference is that $t_1$ has $m$ where $t_2$ has $n$. In particular $m=n$ implies $S(m)=S(n)$ -- and this is viewed as a fact about equality, not one about the successor function.
So since $m=n\to S(m)=S(n)$ is a logical truth, the claims $$ S(m)=S(n) \leftrightarrow m=n \qquad\text{and}\qquad S(m)=S(n) \to m=n $$ are logically equivalent; it is mostly a matter of temperament whether one states one or the other as an axiom.
The formulation with $\leftrightarrow$ has the arguable advantage that it contains more explicit information, particularly for a reader who is not concerned with the subtleties of how logic treats equality.
The formulation with $\to$ is on the other hand a simpler formula -- especially if we view $\varphi\leftrightarrow \psi$ as an abbreviation for $(\varphi\to\psi)\land(\psi\to\varphi)$ -- so it will often be preferred in the name of making the axioms as short as possible.