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. 

(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](https://en.wikipedia.org/wiki/Beth_definability).)

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, $\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$? 

I expect the answer is **No**, but I don't know how to prove this.