Question about Successor Function

[agapito]

One of the Peano Axioms specifies

Sa = Sb --> a = b

where S is the successor function. How does one establish from the axioms that S is, in fact, a function, that is the converse

a = b --> Sa = Sb?

Probably a very simple matter, but I would appreciate any help in clarifying. Many thanks in advance,

Agapito

 

[HOI]

That should be part of the definition! If we say, as part of, say, the Peano axioms, "there exist a successor function" then we are saying this is a function. The Wikipedia entry on the Peano axioms say ". The naturals are assumed to be closed under a single-valued "successor" function S." (my emphasis)

 

[Evgeny.Makarov]

Peano Arithmetic is by definition a theory with equality. One of the equality axioms is $x=y\to f(x)=f(y)$ for all functional symbols of arity 1, and similarly for other arities.