Can the subsitution property be deduced from the peano axioms? How does the substitution property of equality, i.e. for any function on the naturals $f : \mathbb{N} \to \mathbb{N}$,
$$ \forall a \in \mathbb{N} . \: \forall b \in \mathbb{N} . \; a = b \implies f(a) = f(b)$$
follow from the Peano axioms?
Wikipedia gives Peano axioms 2-5 as

*

*Every natural number $x$, $x = x$. That is, equality is reflexive.

*For all natural numbers $x$ and $y$, if $x = y$, then $y = x$. That is, equality is symmetric.

*For all natural numbers $x$, $y$ and $z$, if $x = y$ and $y = z$, then $x = z$. That is, equality is transitive.

*For all $a$ and $b$, if $b$ is a natural number and $a = b$, then a is also a natural number. That is, the natural numbers are closed under equality.

(source)
These define equality to be an equivalence relation, but that isn't sufficient to entail the substitution principle. That's easy to see as we can define equivalence relations on natural numbers that don't obey the substitution principle. For example, let $n \approxeq m$ if $n$ and $m$ share the same first digit in base-10. $\approxeq$ is an equivalence relation, since it's reflexive, symmetric and transitive. However we also have
$$
10 \approxeq 19
$$
but
$$
1 + 10 \not\approxeq 1 + 19,
$$
so it does not have the substitution property.
Wikipedia does note that axioms 2-5 are usually excluded from a modern treatment as they are defined in first-order logic with equality (which takes the substitution principle as axiomatic).
Is the Wikipedia missing the substitution principle, or is it possible to deduce it from the other axioms?
 A: If we consider the first-order theory of arithmetic, the usual approach is to consider equality part of underlying logic.
But we can use an underlying logic without equality, in which case a suitable version of axioms are necessary to prove the usual substitution properties of equality.
Using transitivity (at least a part of it), two axioms regarding the successor function $s$, i.e. $a=b \to s(a)=s(b)$ and $s(a)=s(b) \to a=b$, as well as Induction and axioms for $+,\times$, we can prove refelxivity, simmetry and the general form of substitution (for functions and formulas).
Details can be found into Kleene, Introduction to Metamathematics (1952) page 183.
Transitivity is postulated in the form: $\vdash a=b \to (a=c \to b=c)$.
From it, written as: $(a+0=a) \to (a+0=a \to a=a)$, using the axiom for $+$ : $a+0=a$, and Modus Ponens we get: $\vdash a=a$.
Similarly, from transitivity in the form $ a=b \to (a=a \to b=a)$, using the newly proved: $a=a$ we get: $\vdash a=b \to b=a$. And so on.
The next step is to prove substitution with $+$, starting from: $\vdash a = b \to a + c = b + c$. The proof is by induction on $b$.
In this way, working step-by-step, we can prove all relevant property regarding $=$, up to the general results:

$r=s \to t[r/x]= t[s/x]$, and


$r=s \to \varphi [t/x] \leftrightarrow \varphi [s/x]$.

Note: terms substitution, written in modern form, is: if $\vdash \varphi$, then $\vdash \varphi [t/x]$y, with suitable proviso regarding  substitutability, and it follows from Genarlization and quantifier axiom: $\vdash \forall \varphi \to \varphi [t/x]$.
