Motivation: Many "weak" arithmetic functions and/or relations ("relations" for short) are equivalent with relations explicitly definable by relations which were recursively defined by them beforehand (let's call these "explictly re-definable"). I wonder whether this is so for all relations or whether and why e.g. addition is not explicitly re-definable by multiplication (and what this means).
Definition 1: A relation $f$ is recursively weaker than $g$ when $g$ is recursively definable by $f$ (see picture below, left): $f \leq_{\mathsf{rec}} g$
Definition 2: A relation $f$ is explicitly weaker than $g$ when $f$ is explicitly re-definable by $g$ (see picture below, right): $f \leq_{\mathsf{exp}} g$
Note that both relations are transitive.
Recursive definitions (left) and explicit re-definitions (right)1:
$$\begin{array}{llll} \small{(1)} &\small{n < n'} &\small{(6)} & \small{m = n' \Leftrightarrow n < m \wedge \neg(\exists x)\ n < x < m} \\ &\small{n < m \Rightarrow n < m'} & \small{(7)}& \small{m = n' \Leftrightarrow m = n + 1} \\ \small{(2)} &\small{n + 0 = 0} & \small{(8)}& \small{n < m \Leftrightarrow (\exists x \neq 0)\ n + x = m} \\ &\small{n + m' = (n+m)'} & \small{(9)}& \small{n < m \Leftrightarrow n \operatorname{mod} m = n } \\ \small{(3)} &\small{n \operatorname{div} n} &\small{(10)} & \small{n \operatorname{div} m \Leftrightarrow m \operatorname{mod} n = 0} \\ &\small{n \operatorname{div} m \Rightarrow n \operatorname{div} (m + n)} & \small{(11)}& \small{n \operatorname{div} m \Leftrightarrow (\exists x)\ n \times x = m} \\ \small{(4)} &\small{0 \operatorname{mod} n = 0} & & \\ &\small{(m \operatorname{mod} n)' = m \Rightarrow m' \operatorname{mod} n = 0} & & \\ &\small{(m \operatorname{mod} n)' \neq m \Rightarrow m' \operatorname{mod} n = (m \operatorname{mod} n)'} & & \\ \small{(5)} &\small{n \times 0 = 0} & & \\ &\small{n \times (m + 1) = (n \times m) + n } & & \\ \end{array}$$
There are some missing links in the picture, esp. there seems to be no obvious explicit re-definition of
$\operatorname{succ}$ by $\times$
$\operatorname{mod}$ by $\times$
$+$ by $\times$
$+$ by $\operatorname{mod}$
$+$ by $\operatorname{div}$
(at least not obvious to me).
In the case of $+$ and $\times$ I doubt that there will be a explicit re-definition. Look how and why $+$ has to be defined recursively by $\operatorname{succ}$. It's because you cannot capture the following (only seemingly explicit) naive definition otherwise:
$$n + m = k \Leftrightarrow \operatorname{succ}^n(\operatorname{succ}^m(0)) = \operatorname{succ}^k(0)$$
Trying to re-define $+$ by $\times$ explicitly you will probably come up with
$$n + m = k \Leftrightarrow \operatorname{double}^n(\operatorname{double}^m(1)) = \operatorname{double}^k(1)$$
with $\operatorname{double}(n) = n \times 2$. (Compare this with $\operatorname{succ}(n) = n +1$.)
But this is not a proof that it is impossible to re-define $+$ by $\times$ (or by $\operatorname{mod}$ maybe).
So I am looking either
for an explicit re-definition of $+$ by $\times$ (or by $\operatorname{mod}$)
or
for a proof that no such re-definition can exist.
[ADDENDUM] In the light of Joel's and Andreas' answer: Is it obvious that $\times$ cannot re-define the weaker relations $<$ and $\operatorname{succ}$ (both re-definable by $+$), neither?
1 We write $n'$ for $\operatorname{succ}(n)$. Note that in (4) $n \neq 0$ is assumed.
