# The (un)decidability of Robinson-Arithmetic-without-Multiplication?

Take our old friend Robinson Arithmetic, and cut it down to a theory of successor and addition.

To spell that out (just to ensure that we are singing from the same hymn sheet), take the first-order theory with $\mathsf{0}$ as the sole constant, and $\mathsf{S}$ and $+$ as the built-in function signs, with the five axioms

1. $\mathsf{\forall x\ 0 \neq Sx}$
2. $\mathsf{\forall x\forall y\ Sx = Sy \to x = y}$
3. $\mathsf{\forall x(x \neq 0 \to \exists y\ x = Sy)}$
4. $\mathsf{\forall x\ (x + 0) = x}$
5. $\mathsf{\forall x\forall y\ (x + Sy) = S(x + y)}$

and whose deductive system is your favourite classical first-order logic with identity.

Since this cut-down theory doesn't represent the recursive functions, you can't use the usual proof of undecidability for an arithmetic. Since this cut-down theory doesn't even know that addition is commutative, i.e. can't prove $\mathsf{\forall x\forall y\ x = y = y + x}$, you can't do the kind of manipulations inside the theory involved in a quantifier-elimination proof of decidability (cf. what happens when we add induction to this theory to get Presburger arithmetic, i.e. Peano Arithmetic minus multiplication).

Ermmmm .... so .... Drat it, I ought to know how to prove that this cut-down theory is decidable or that it is undecidable. But I seem to have forgotten, assuming I ever knew, and searching around hasn't helped me out. OK folks, I'm more than likely to be having a senior moment here -- so be gentle! -- but how do we show the theory is (un)decidable?

• "Since this cut down theory doesn't even know that addition is commutative..." I think you've given an interpretation to the operation "+" which the formal system doesn't have. – Doug Spoonwood Jul 21 '14 at 14:22
• The Wikipedia says this en.wikipedia.org/wiki/Robinson_arithmetic "The first incompleteness theorem applies only to axiomatic systems defining sufficient arithmetic to carry out the necessary coding constructions (of which Gödel numbering forms a part). The axioms of Q [Robinson arithmetic] were chosen specifically to ensure they are strong enough for this purpose. Thus the usual proof of the first incompleteness theorem can be used to show that Q is incomplete and undecidable." – Doug Spoonwood Jul 21 '14 at 14:30
• @DougSpoonwood Yes of course Q is undecidable. But a sub theory of an undecidable theory can be decidable. So the undecidability of Q doesn't settle the question I'm asking. – Peter Smith Jul 21 '14 at 16:02
• Oops! Sorry, I misread your question. – Doug Spoonwood Jul 21 '14 at 16:39
• I haven't worked out the details, but I suspect that the theory is undecidable, since the $+$ function is so unrestricted. You may be able to use the fact that the theory of an arbitrary binary function is undecidable. – Alex Kruckman Jul 21 '14 at 19:23

Consider the model $\mathfrak{M}$ with domain the natural numbers $\mathbb{N}$ plus one more object, say $a$. Define $S$ on $\mathbb{N}$ normally and $Sa=a$. Define $+$ on $\mathbb{N}$ normally and $x+a=a+x=a$ for all $x \in \mathfrak{M}$.

Then it is quite easy to prove that $\mathfrak{M}$ is a model of the $5$ axioms in which the statement $\varphi$, "there exists an $x$ such that $Sx=x$" is true.

So $\varphi$ cannot be decided by the axioms since in the standard model it is false and true here, so the theory is undecidable.

• What you're arguing here is that the theory is incomplete, not that it is undecidable. Decidability in this context means whether there is an algorithm that tells whether or not a given formula is a theorem. A complete theory is decidable (just search for proofs and disproofs in parallel), but the converse is not necessarily the case. – Henning Makholm Oct 30 '14 at 17:23

It is undecidable.

Let $\mathcal L$ be the first-order language with equality and one binary predicate $p({-},{-})$ and no constants or function symbols. Call an $\mathcal L$-sentence of the form $\varphi\land \exists x\exists y(x\ne y)$ "fancy" -- it is then well known that satisfiability of fancy sentences is undecidable.

Consider the following translation from $\mathcal L$ into the your additive Robinson arithmetic:

$$\overline{\varphi\land\psi} \equiv \overline\varphi\land\overline \psi \qquad \overline{\neg\varphi} \equiv \neg\overline\varphi$$ $$\overline{\exists x.\varphi} \equiv \exists x(x=\mathsf S x \land \overline\varphi) \qquad \overline{x=y} \equiv x=y$$ $$\overline{p(x,y)} \equiv x+y=x$$

Now clearly if $\varphi$ is a fancy sentence and $\overline{\varphi}$ is consistent with additive Robinson arithmetic, then $\varphi$ is satisfiable -- it is trivial to derive a model of the latter from a model of the former; the domain will be the elements that are their own successors.

On the other hand if $\varphi$ is a satisfiable fancy sentence, then there's a model of additive Robinson arithmetic that satisfies $\overline\varphi$, as follows:

Let $(A,p)$ be a model of $\varphi$; without loss of generality take $A$ to be disjoint from $\mathbb N$. Because $\varphi$ is fancy $A$ has at least two elements, so let $f:A\to A$ be such that $f(a)\ne a$ for all $a\in A$. Now construct an model of additive Robinson arithmetic with domain $\mathbb N\cup A$, as follows: $$0 = 0$$ $$\mathsf S n = (n+1) \qquad \mathsf Sa = a$$ $$n\oplus n' = (n+n') \qquad a\oplus n= n\oplus a = a \qquad a\oplus a' = \begin{cases} a & \text{when }p(a,a') \\ f(a) & \text{otherwise} \end{cases}$$