We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)b=(Sa)c &\to b=c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$ As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model. We prove by induction that for all $m$ and $n$, the axioms imply $S^m0\ S^n0=S^{mn}0$, will determine the values of the multiplication function for the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$. - The case $m=0$ follows from the first axiom. - The case $m>n$ follows from $m'=n,n'=m$. - The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array} - The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$. - In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} So either immediately or by cancelling $S^j0$ from both sides, $S^m0\ S^n0 = S^{mn}0$.