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?

  • $\begingroup$ "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. $\endgroup$ Jul 21, 2014 at 14:22
  • $\begingroup$ 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." $\endgroup$ Jul 21, 2014 at 14:30
  • $\begingroup$ @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. $\endgroup$ Jul 21, 2014 at 16:02
  • $\begingroup$ Oops! Sorry, I misread your question. $\endgroup$ Jul 21, 2014 at 16:39
  • $\begingroup$ 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. $\endgroup$ Jul 21, 2014 at 19:23

2 Answers 2


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}$$


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.

  • 4
    $\begingroup$ 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. $\endgroup$ Oct 30, 2014 at 17:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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