Is multiplication implicitly definable from successor? A relation $R$ is implicitly definable in a structure $M$ if there is a formula $\varphi(\dot R)$ in the first-order language of $M$ expanded to include relation $R$, such that $M\models\varphi(\dot R)$ only when $\dot R$ is interpreted as $R$ and not as any other relation. In other words, the relation $R$ has a first-order expressible property that only it has.
(Model theorists please note that this is implicit definability in a model, which is not the same as the notion used in Beth's implicit definability theorem.)
Implicit definability is a very weak form of second-order definability, one which involves no second-order quantifiers. Said this way, an implicitly definable relation $R$ is one that is definable in the full second-order Henkin structure of the model, but using a formula with only first-order quantifiers.
Examples. Here are some examples of relations that are implicitly definable in a structure, but not definable.

*

*The predicate $E$ for being even is implicitly definable in the language of arithmetic with successor, $\langle\mathbb{N},S,0\rangle$. It is implicitly defined by the property that $0$ is even and evenness alternates with successor: $$E0\wedge \forall x\ (Ex\leftrightarrow\neg ESx).$$ Meanwhile, being even is not explicitly definable in $\langle\mathbb{N},S,0\rangle$, as that theory admits elimination of quantifiers, and all definable sets are either finite or cofinite.


*Addition also is implicitly definable in that model, by the usual recursion $a+0=a$ and $a+(Sb)=S(a+b)$. But addition is not explicitly definable, again because of the elimination of quantifiers argument.


*Multiplication is implicitly definable from addition in the standard model of Presburger arithmetic $\langle\mathbb{N},+,0,1\rangle$. This is again because of the usual recursion, $a\cdot 0=0$, $a\cdot(b+1)=a\cdot b+a$. But it is not explicitly definable, because this theory admits a relative QE result down to the language with congruence mod $n$ for every $n$.


*First-order truth is implicitly definable in the standard model of arithmetic $\langle\mathbb{N},+,\cdot,0,1,<\rangle$. The Tarski recursion expresses properties of the truth predicate that completely determine it in the standard model, but by Tarski's theorem on the nondefinability of truth, this is not a definable predicate.
My question concerns iterated applications of implicit definability. We saw that addition was implicitly definable over successor, and multiplication is implicitly definable over addition, but I don't see any way to show that multiplication is implicitly definable over successor.
Question. Is multiplication implicitly definable in $\langle\mathbb{N},S,0\rangle$?
In other words, can we express a property of multiplication $a\cdot b=c$ in its relation to successor, which completely determines it in the standard model?
I expect the answer is No, but I don't know how to prove this.
Update. I wanted to mention a promising idea of Clemens Grabmayer for a Yes answer (see his tweet). The idea is that evidently addition is definable from multiplication and successor (as first proved in Julia Robinson's thesis, and more conveniently available in Boolos/Jeffrey, Computability & Logic, Sect. 21). We might hope to use this to form an implicit definition of multiplication from successor. Namely, multiplication will be an operation that obeys the usual recursion over addition, but replacing the instances of $+$ in this definition with the notion of addition defined from multiplication in this unusual way. What would remain to be shown is that there can't be a fake version of multiplication that provides a fake addition, with respect to which it fulfills the recursive definition of multiplication over addition.
 A: Contrary to my initial expectation, the answer is Yes.
This answer is based on the idea of Clemens Grabmayer, which makes the observation that addition $+$ is definable from multiplication $\cdot$ and successor.
The idea generalizes to the following:
Theorem. Suppose that relation $R$ is implicitly definable in model $M$, that $S$ is implicitly definable in the expansion $\langle M,R\rangle$, and that $R$ is explicitly definable in $\langle M,S\rangle$. Then $S$ is implicitly definable in $M$.
Proof.
Suppose that $R$ is the unique relation fulfilling sentence $\varphi(\dot R)$ in $M$, in the language expanded with predicate $\dot R$. Suppose $S$ is the unique relation fulfilling sentence $\psi(R,\dot S)$ in $\langle M,R\rangle$. And suppose that $R$ is definable by formula $\theta(x,S)$ in $\langle M,S\rangle$, in that $Rx\leftrightarrow\theta(x,S)$.
Let $\Phi(\dot S)$ be the sentence asserting:

*

*$\varphi(\theta(x,\dot S))$, that is, the relation defined by $\theta(x,\dot S)$ fulfills property $\varphi$, and

*$\psi(\theta(x,\dot S),\dot S)$ holds, that is, the assertion $\psi(\dot R,\dot S)$ holds where $\dot R$ is interpreted by the relation defined by $\theta(x,\dot S)$.

I claim that this is an implicit definition of $S$ in $M$. The reason is that whatever relation interpretation is given to $\dot S$, it will have the property that the relation extracted from it via $\theta(x,\dot S)$ will have to be $R$, since it fulfills the implicit definition of $R$ given by $\varphi$. And further, since $\Phi$ asserts that $\psi$ is fulfilled by $\dot S$ relative to that relation, it follows that $\dot S$ must be $S$. $\Box$
The corollary is that:
Corollary. Multiplication is implicitly definable from successor.
Proof. Addition is implicitly definable in $\langle\mathbb{N},S,0\rangle$, and multiplication is implicictly definable over addition $\langle\mathbb{N},S,0,+\rangle$, and by the Boolos/Jeffrey observation, addition is explicitly definable from multiplication and successor. So we are in the case of the theorem. $\Box$
A more striking instance might be:
Corollary. First-order arithmetic truth for the standard model of arithmetic $\langle\mathbb{N},+,\cdot,0,1<\rangle$ is implicitly definable just from successor $\langle\mathbb{N},S,0\rangle$.
Proof. I intend to use the trinary truth predicate $\text{Tr}(\varphi,x,y,z)$, holding when $\mathbb{N}\models\varphi[x,y,z]$. This truth predicate is uniquely characterized on the standard model $\mathbb{N}$ by fulfilling the Tarski recursion, and so it is implicitly definable in $\langle\mathbb{N},+,\cdot\rangle$. But both addition and multiplication are definable from the truth predicate (this is why we use the trinary version, since with just successor we don't initially have any coding, but once we get $+$ and $\times$, then the usual coding kicks in), and they themselves are implicitly definable from successor. So by the theorem, truth is implicitly definable from successor. $\Box$
And one can of course iterate this by forming the predicate for truth-about-truth, and truth-about-truth-about-truth and so on, proceeding transfinitely up the hierarchy for quite some way.
But lastly, let me mention that the theorem falls short of proving that the property of being implicitly-definable-over is transitive. That seems to be false in light of counterexamples discussed in the comments.
A: 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)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 that the only possible value for $S^m0\ S^n0$ is $S^{mn}0$, and thus determine the multiplication function on 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
\end{array}
Since $S^m0\ S^n=0$ is an element of the standard model, it is of the form $S^p0$. So also
\begin{array}{rll}
S^j0\ S^m0\ S^n0 &= S^j0 S^p0 & \text{ by definition of }p\\
&= S^{jp}0 &\text{ by }m'=j, n'=p
\end{array}
Now $S^{mjn}0=S^{jp}0$, $mjn=jp$, $p=mn$, and $S^m0\ S^n0 = S^{mn}0%$ as desired.
This establishes the claim that the above axioms implicitly define multiplication in $(\mathbb{N}, 0, S)$.
