4
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

This is called monadic second-order logic.

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

Thus, the answer to Tarski’s question is negative.

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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.) $\endgroup$
    – Hans-Peter Stricker
    Commented Aug 25, 2014 at 17:24
  • $\begingroup$ 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 $\endgroup$
    – Emil Jeřábek
    Commented Aug 25, 2014 at 17:44
  • 2
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Aug 25, 2014 at 17:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .