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.

  • 5
    $\begingroup$ Ever since I heard your story about Hugh sending you to disprove something, and you coming back with a proof, I always expect when "I expect the answer is no" to have someone come in and say "Oh, it's yes, and here's the proof". $\endgroup$
    – Asaf Karagila
    Jul 9, 2022 at 13:35
  • 3
    $\begingroup$ Is there an obvious example that implicit definability isn't transitive (that is, $A$ is i.d. over $\mathcal{M}[B]$ and $B$ is i.d. over $\mathcal{M}$ but $A$ isn't i.d. over $\mathcal{M}$)? $\endgroup$ Jul 9, 2022 at 14:12
  • 4
    $\begingroup$ @NoahSchweber This was going to be my example for that. $\endgroup$ Jul 9, 2022 at 14:34
  • 3
    $\begingroup$ Meanwhile, Clemens Grabmeyer has an interesting proposal for a positive answer (see twitter.com/clegra/status/1545771851586146304). The idea is that + is definable from S and $\cdot$. $\endgroup$ Jul 9, 2022 at 14:36
  • 3
    $\begingroup$ @JoelDavidHamkins While it's not actually an answer, would you mind if I added the non-transitivity example as an answer (for relative permanence and accessibility)? $\endgroup$ Jul 10, 2022 at 0:39

2 Answers 2


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.

  • 1
    $\begingroup$ Does this mean that all recursive functions are explicitly definable in terms of a relation implicitly definable in terms of successor? $\endgroup$ Jul 9, 2022 at 17:21
  • 1
    $\begingroup$ My guess is that there is a single $n$-ary relation (roughly a universal Turing machine plus some extra features) which (1) is implicitly definable from successor and (2) can explicitly define any recursive function. In which case implicit definition is quite powerful. :) $\endgroup$ Jul 9, 2022 at 17:32
  • 4
    $\begingroup$ Yes, we have that already, since truth is implicitly definable over +, *. But that doesn't seem to answer the question. $\endgroup$ Jul 9, 2022 at 17:34
  • 1
    $\begingroup$ In terms of your desire for a transitivity counterexample: primes is definable in terms of multiplication, but is not implicitly definable in terms of successor. $\endgroup$ Jul 9, 2022 at 18:07
  • 7
    $\begingroup$ Called it! $\endgroup$
    – Asaf Karagila
    Jul 10, 2022 at 3:13

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)$.

  • 2
    $\begingroup$ Thank you very much for this. $\endgroup$ Jul 10, 2022 at 12:41
  • $\begingroup$ Matt, can multiplication be implicitly defined with only equalities? (i.e., can the cancelation rule be replaced with just simple equalities?) $\endgroup$ Jul 10, 2022 at 17:15
  • $\begingroup$ Can you clarify the inductive strategy? I don't see what the implied well-ordering of $\mathbb{N}\times\mathbb{N}$ that will make the induction work is supposed to be. $\endgroup$
    – zeb
    Jul 10, 2022 at 23:13
  • $\begingroup$ @zeb, thanks for asking, and let me know if it makes sense now. I knew I had all the ingredients before, but it took a while to see the clear case distinction on whether $(m-1,n)=1$. $\endgroup$
    – user44143
    Jul 11, 2022 at 17:46
  • 1
    $\begingroup$ You can drop the cancellation law: if you have $S^m0 S^n0 = S^p0$, then your last case proves that $S^j0 S^p0 = S^j0 S^{mn}0$, but since $j < m$ you can apply the inductive hypothesis to see that this implies $jp = jmn$, and thus that $p = mn$. $\endgroup$
    – zeb
    Jul 12, 2022 at 3:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.