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 itthis is a finite extension of your theory$T'$ (modulo the translation of $Sx$ by $x+a$), your theorythe latter is also undecidable. Note that this
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 relies on your statement.
Let $M$ be the set of axiom 1affine functions $f\colon\mathbb Z\to\mathbb Z$ of the form $f(x)=ax+b$, where $x \neq Sx$$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 differs fromimplies 2, and axioms 1 and 3 are consequence of the usual axiomfact that $Sx\ne0$$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 Robinson arithmeticthe 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$.
