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 math.se 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 ...]

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

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

  • 3
    $\begingroup$ Apologies -- that original Axiom 1 was indeed a silly typo. (Talk about senior moments ....) $\endgroup$ – Peter Smith Jul 25 '14 at 12:01
  • $\begingroup$ @EmilJerabek: Interesting. What would be an example of a wff $W$ definable in the language of this subtheory of $Q$ theory such that neither $W$ nor $\lnot $$W$ are provable in this subtheory? $\endgroup$ – Thomas Benjamin Dec 14 '15 at 4:21
  • $\begingroup$ @ThomasBenjamin: The most obvious one is commutativity of addition. $\endgroup$ – Emil Jeřábek Dec 14 '15 at 10:32
  • $\begingroup$ @EmilJeřábek: Interesting. If you interpreted '+' as concatenation and added the "Editor Axiom" to the list, could you prove commutativity then? Why don't the axioms of equality and Ax2 suffice? $\endgroup$ – Thomas Benjamin Dec 14 '15 at 12:16
  • 1
    $\begingroup$ (1) What is the “Editor Axiom”? (2) Ax2 says that $1$ is a right-cancellative element. This has nothing to do with commutativity. (3) Presburger arithmetic is the complete theory of the commutative structure $(\mathbb N,0,1,+)$, hence it of course proves commutativity. (It’s even often included as an axiom, though likely not in your axiomatization if it includes the induction schema. In any case a proof from the axioms should not be difficult.) $\endgroup$ – Emil Jeřábek Dec 14 '15 at 16:47

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.