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.

18more comments