So I was hoping to get some help verifying my proof that $(\mathbb{Z}, s)$ admits quantifier elimination. I am hoping to use this to get a 'feel' for these sorts of proofs and theorem.
My attempt is to use the following theorem in David Marker's book.
"Let $T$ be a $L$-theory. Suppose for every quantifier-free, $\theta(\bar v, w)$, there is a quantifier-free $\psi(\bar v)$ such that $T\models\exists w\ \theta(\bar v, w)\leftrightarrow \psi(\bar v)$, then $T$ admits quantifier elimination"
So all we have to show is that Th($\mathbb{Z}$) in the language consisting of only the succesor function, $s$, can eliminate a single existential quantifier. I would like to induct on $\theta(\bar v, w)$ minus the quantifer case.
So for atomic case: We have $\mathbb{Z} \models \exists b\ s^n(x) = s^m(b)$, for the forward implication we can let it be the tautology $s^n(x) = s^n(x)$. For the backward implication, $s^n(x) = s^n(x) \rightarrow \exists b\ s^n(x) = s^m(b)$ because $\mathbb{Z}$ has no end points, we can always find some guy to the left of (any) $x$ and 'reach it'.
After the atomic case, if nothing goes wrong, the Induction hypothesis should get us through the inductive step.
So is my attempt valid ? If it is wrong, any hints to point me in the right direction is deeply appreciated.
Cheers !