Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question

1 Answer 1

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.

share|improve this answer
    
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.) –  Hans Stricker Aug 25 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 –  Emil Jeřábek Aug 25 at 17:44
2  
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. –  Emil Jeřábek Aug 25 at 17:50
    
Thanks, Emil, this rounds off the picture. –  Hans Stricker Aug 25 at 21:31

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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