Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

I asked this over at math.stackexchange, and though a number of people were interested enough to vote up the question, I didn't get an answer -- which makes me wonder whether it isn't quite so trivial/dumb as I originally feared it was. So let me try again in this more turbo-charged forum ...

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, 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 [well, given the lack of answers on maybe a forgivable senior moment?] -- so be gentle! -- but how do we show the theory is (un)decidable? [My bet is on undecidable, for what little that it is worth ...]

share|cite|improve this question
Robinson arithmetic has $Sx\ne0$ in place of your axiom 1. Is this change intentional? –  Emil Jeřábek Jul 25 '14 at 11:23
Oops that was a typo! –  Peter Smith Jul 25 '14 at 11:58

1 Answer 1

up vote 15 down vote accepted

The theory $T'$ with axiom $Sx\ne x$ in place of $Sx\ne0$, as it was originally written, is undecidable, because the theory of groups with a distinguished nonidentity element $a$ is a conservative extension of the theory of nontrivial groups, shown undecidable by Tarski. Since this is a finite extension of $T'$ (modulo the translation of $Sx$ by $x+a$), the latter is also undecidable.

The theory with the proper axiom $Sx\ne0$ is undecidable as well. The reduction above doesn’t quite work as the offending axiom is incompatible with groups, nevertheless one can apply a minor modification of Tarski’s original argument.

Let $M$ be the set of affine functions $f\colon\mathbb Z\to\mathbb Z$ of the form $f(x)=ax+b$, where $a\in\mathbb N^{>0}$, $b\in\mathbb Z$, and if $a=1$, also $b\ge0$. It is easy to see that $M$ is closed under composition, and contains the identity and the function $s(x)=x+1$. The structure $$\mathcal M=\langle M,\mathrm{id},\circ,S\rangle,$$ where $S(f)=f\circ s$, satisfies axioms 1–5: in particular, $f\circ s=g\circ s$ implies $f=f\circ s\circ s_{-1}=g\circ s\circ s_{-1}=g$ where $s_n(x)=x+n$, which implies 2, and axioms 1 and 3 are consequence of the fact that $f\circ s_{-1}\in M$ iff $f\ne\mathrm{id}$.

It thus suffices to prove that $\mathrm{Th}(\mathcal M)$ is hereditarily undecidable, and we can do this by interpreting $\langle\mathbb N,+,\cdot\rangle$ in $\mathcal M$. We embed $\mathbb N$ in $\mathcal M$ via $n\mapsto s_n$. The range of the embedding is definable, as $f\in M$ is of the form $s_n$ for some $n$ if and only if it commutes with $s$. Addition on $\mathbb N$ is definable in $\mathcal M$ as $s_{n+m}=s_n\circ s_m$. Finally, notice that if $f(x)=ax+b$, we have $f\circ s_n=s_{an}\circ f$, hence $$nm=k\iff\forall f\in M\,(f\circ s=s_n\circ f\to f\circ s_m=s_k\circ f)$$ for $n>0$. This shows that multiplication on $\mathbb N$ is definable in $\mathcal M$.

share|cite|improve this answer
Apologies -- that original Axiom 1 was indeed a silly typo. (Talk about senior moments ....) –  Peter Smith Jul 25 '14 at 12:01

Your Answer


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.