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?
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.