Return to Revisions

No, the structure is definitionally equivalent with $(\mathbb Z,0,S)$ (that is, you make the successor function a function rather than a predicate), which is well-known to have elimination of quantifiers: every formula is equivalent to a Boolean combination of formulas of the form $y=S^n(x)$, where $x,y$ are either variables or $0$, and $n$ is a natural number. For formulas with one free variable, this means that the only definable subsets are finite or cofinite.