44

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
    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". – Asaf Karagila Jul 09 '22 at 13:35
  • That would be great! – Joel David Hamkins Jul 09 '22 at 13:41
  • 3
    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}$)? – Noah Schweber Jul 09 '22 at 14:12
  • 4
    @NoahSchweber This was going to be my example for that. – Joel David Hamkins Jul 09 '22 at 14:34
  • @JoelDavidHamkins What about taking $\mathcal{M}$ to be $(\mathbb{N};+,\times)$, $B$ to be the truth predicate for arithmetic, and $A$ to be something like the Turing jump of $B$? – Noah Schweber Jul 09 '22 at 14:35
  • 3
    Meanwhile, Clemens Grabmeyer has an interesting proposal for a positive answer (see https://twitter.com/clegra/status/1545771851586146304). The idea is that + is definable from S and $\cdot$. – Joel David Hamkins Jul 09 '22 at 14:36
  • @JoelDavidHamkins Ah, that's quite nice, I'd started thinking along those lines but didn't see how to get $+$ from $S$ and $\cdot$ so I dropped it. – Noah Schweber Jul 09 '22 at 14:37
  • I don't think the proposal about jump-of-truth works, since truth is definable from the jump and so we can make a single implicit definition, even for truth about truth. – Joel David Hamkins Jul 09 '22 at 14:37
  • "truth is definable from the jump" What do you mean by that? Truth isn't definable, but the jump is. That said, you're right that my idea doesn't work: everything hyperarithmetic is (reducible to something which is) i.d. over $\mathbb{N}$. – Noah Schweber Jul 09 '22 at 14:37
  • 1
    If I have an oracle for the jump of truth, I can define the truth predicate. So I can implicitly define that the jump has the property that the definition obeys the Tarski recursion, and that it is the jump of it. – Joel David Hamkins Jul 09 '22 at 14:38
  • 1
    Ah, now I see; yes, that's right, and gives the hyperarithmeticity result in my previous comment. Sorry, I was misinterpreting what you meant by "jump" there! – Noah Schweber Jul 09 '22 at 14:39
  • 1
    Hm, what about the following: still take $B$ to be truth, but now have $A$ be a sufficiently generic real (since ${\bf 0^{(\omega)}}$ lets us define lots of those). Genericity might prevent $A$ from being i.d. over $\mathbb{N}$. – Noah Schweber Jul 09 '22 at 14:43
  • Incidentally, for the set theorists, one can iterate the implicit definability operator to form an implicit analogue of L. We call it Imp, and see more here: https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-57/issue-3/Algebraicity-and-Implicit-Definability-in-Set-Theory/10.1215/00294527-3542326.full – Joel David Hamkins Jul 09 '22 at 14:43
  • Noah, I think that example works to show intransitivity. With the truth predicate we can define Cohen real that is generic wrt all definable dense sets. But no such real can be implicitly definable, since if phi(G), then there will be some condition forcing this, in which there will be other reals also fulfilling phi. – Joel David Hamkins Jul 09 '22 at 14:52
  • Yes, I think so too. (OK, so now: is there a natural example of intransitivity?) – Noah Schweber Jul 09 '22 at 14:57
  • I prefer to ask: is there a simpler, more elementary example? – Joel David Hamkins Jul 09 '22 at 14:59
  • Is there a typo in the first example, namely the second occurrence of $\langle \mathbb{N}, S, 0\rangle$? – Andrej Bauer Jul 09 '22 at 16:22
  • I don't see a typo there---what did you have in mind? Being even is implicitly but not explicitly definable in that structure. – Joel David Hamkins Jul 09 '22 at 16:26
  • The answer is yes. The suggestion of Clemens seems to work. I am posting an answer now. – Joel David Hamkins Jul 09 '22 at 16:34
  • 3
    @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)? – Noah Schweber Jul 10 '22 at 00:39
  • 2
    Yes, please go ahead. – Joel David Hamkins Jul 10 '22 at 00:42
  • 2
    That last example, of first-order truth being implicitly but not explicitly definable in $(\Bbb N,+,\cdot,0,1,<)$, is really interesting. Is there a simpler example of this, of an implicit definition (that you'd be willing to explicitly write out) that defines only one relation which cannot be explicitly defined from that theory? – Akiva Weinberger Jul 10 '22 at 02:35
  • @NoahSchweber Actually, I have a new plan. I have asked a question specifically about transitivity, and I would encourage you to post the forcing answer there. https://mathoverflow.net/q/426359/1946 – Joel David Hamkins Jul 10 '22 at 12:33

2 Answers2

25

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
    Does this mean that all recursive functions are explicitly definable in terms of a relation implicitly definable in terms of successor? – Geoffrey Irving Jul 09 '22 at 17:21
  • Good question. I don't see that this follows, since perhaps we have a PR function that isn't quite able to explicitly define the prior functions needed to realize it. But I have no counterexample. – Joel David Hamkins Jul 09 '22 at 17:27
  • 1
    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. :) – Geoffrey Irving Jul 09 '22 at 17:32
  • 4
    Yes, we have that already, since truth is implicitly definable over +, *. But that doesn't seem to answer the question. – Joel David Hamkins Jul 09 '22 at 17:34
  • 1
    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. – Geoffrey Irving Jul 09 '22 at 18:07
  • That would be great! How do you know primality is not implicitly definable? – Joel David Hamkins Jul 09 '22 at 18:17
  • 1
    Follow-up question about the primes: https://mathoverflow.net/questions/426334/is-the-set-of-primes-implicitly-definable-from-successor. – Geoffrey Irving Jul 09 '22 at 21:00
  • I'm not sure I understand - can you provide the implicit definition, written out explicitly? – Akiva Weinberger Jul 10 '22 at 02:37
  • @AkivaWeinberger, I am writing that up as an answer. –  Jul 10 '22 at 02:50
  • 7
  • 1
    It seems that a lesson of your answer and Fedor Pakhamov's answer about the primes is that the power of the notion of implicit definability depends more drastically than one would think on the number of variables of the relations. Almost no unary relations are implicitly definable over $(\mathbb N, S)$ but incredibly complex $4$-ary relations are. – Will Sawin Jul 12 '22 at 18:07
  • Yes, I was noticing the same thing. I wonder what happens with binary relations? I think with trinary, you could hope to implicitly define a pairing function, and then get the 4-ary relations using it. – Joel David Hamkins Jul 12 '22 at 19:55
22

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
    Thank you very much for this. – Joel David Hamkins Jul 10 '22 at 12:41
  • Matt, can multiplication be implicitly defined with only equalities? (i.e., can the cancelation rule be replaced with just simple equalities?) – Pace Nielsen Jul 10 '22 at 17:15
  • 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. – zeb Jul 10 '22 at 23:13
  • @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$. –  Jul 11 '22 at 17:46
  • Matt, at least the cancellation of successors $Sx=Sy\to x=y$ is automatic, since we are talking about implicit definition in the standard model. – Pace Nielsen Jul 12 '22 at 01:40
  • @Matt Thanks, this looks really good! – zeb Jul 12 '22 at 02:42
  • 1
    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$. – zeb Jul 12 '22 at 03:38
  • Thanks @zeb and Pace for pushing me on this. I (again) think the above list of axioms is now minimal for implicit definability. Meanwhile if we add the axioms \begin{array}{c} Sx\neq0\ Sx=Sy\ \to\ x=y\ y=0\vee (\exists x)(y=Sx)\ (Sa)b=(Sa)c\ \to\ b=c \end{array} the result would be like Raphael Robinson's Theory $Q$ in representing all computable functions and being essentially undecidable. –  Jul 12 '22 at 14:35
  • Beautiful! Surely (???) one can't implicitly define any version of the truth predicate using only universal quantifiers and equalities. – Will Sawin Jul 12 '22 at 18:01
  • @WillSawin, that seems right. Anyway Joel’s proof uses “the Tarski recursion”, which I think includes $$Tr(\ulcorner \forall x \phi\urcorner, 0,y,z) \leftrightarrow \forall x Tr(\ulcorner \phi\urcorner,x,y,z)$$ in the implicit definition, and therefore uses propositional connectives in addition to quantified equations. –  Mar 10 '23 at 12:03