# "Is it possible to give a restricted set-theoretical definition of addition of natural numbers in terms of successor?" [Tarski]

In his paper "Restricted set-theoretical defintions in arithmetic" Raphael Robinson cites a problem posed by Tarski:

Is it possible to give a restricted set-theoretical definition of addition of natural numbers in terms of successor?

More explicitly:

Is it possible to give an explicit definition of addition of natural numbers in terms of successor by a second-order formula where the variables range only over natural numbers or sets of natural numbers?

That means: Is there a formula $\phi(a,b,c)$ of (such restricted) second-order arithmetic such that

$$a + b = c \quad :\equiv \quad \phi(a,b,c)$$

In the same paper Robinson gives a defining formula $\phi_+(a,b,c)$ where the variables may also range over sets of pairs of natural numbers (i.e. not of the required type):

$\qquad a + b = c \quad :\equiv \quad (\forall X)\Big( (0,a) \in X \wedge (\forall (x,y)\in X)\ (x',y')\in X\Big) \rightarrow (b,c) \in X$

Robinson also gives a defining formula $\phi_<(a,b,c)$ of the required type:

$\qquad a < b \quad :\equiv \quad (\exists X)\ a \not\in X \wedge b \in X \wedge (\forall x \in X)\ x' \in X$

At the time of writing his paper, Robinson did not have an answer to Tarski's question.

I wonder if there is an answer today, and what the corresponding proof looks like?

Notice that it can be proved that there is no first-order definition of addition in terms of successor, i.e. by a formula with variables only ranging over natural numbers.

The monadic second-order theory of natural numbers with addition is undecidable, as one can define the divisibility relation $x\mid y$ by $\forall X\,(0\in X\land\forall u\,(u\in X\to u+x\in X)\to y\in X)$, and then one can define multiplication in terms of $+$ and $\mid$ (this is due to Julia Robinson).
On the other hand, the monadic second-order theory of natural numbers with the successor function is decidable by a result of Büchi (generalized to the MSO theory of the full $k$-ary tree in a language with $k$ successors by Rabin).
• There are three results involved: (1) $\mid$ is definable by $+$, (2) $\cdot$ is definable by $+$ and $\mid$, (3) Büchi's result. Is it known which of these results were known to R. Robinson? (Büchi's result most probably not.) Aug 25 '14 at 17:24
• In fact, Büchi provides a description of predicates MSO-definable in $(\mathbb N,0,S)$ in terms of what is now called Büchi automata, and I guess one can use this to show directly that $+$ is not definable. McNaughton’s review seems to indicate that, too: jstor.org/stable/2271342 Aug 25 '14 at 17:44
• Oh, I didn’t see your comment. Büchi’s result is the essential one, and it indeed came later than Robinson’s paper. (1) is obvious, (2) is from 1949 or so and was surely known to Julia Robinson’s husband. You forgot (0) the undecidability of $(\mathbb N,+,\cdot)$, which of course was also known to him. Aug 25 '14 at 17:50