Can successor be defined in $(\mathbb{Z}, +)$?

Question

I once asked whether the successor function can be defined in the structure $(\mathbb{N}, +, 0)$ without parameters. Now, I am asking whether the successor function can be defined in the structure $(\mathbb{Z}, +)$ without parameters. I left out $0$ in that structure because $0$ can certainly be defined without parameters in that structure.

Answer 1

This expands wnoise's comment above into an answer; I've made it CW to avoid reputation gain for their work, and if they post an answer of their own I'll delete this one.

The answer is no, the successor function is not definable in $\mathcal{Z}=(\mathbb{Z};+)$. There is a simple proof of this: the map $$\alpha: z\mapsto-z$$ is an automorphism of $\mathcal{Z}$ which does not preserve the successor operation, but all definable functions(/relations/elements) must be preserved by automorphisms.

Note that this only uses the isomorphism-invariance of first-order logic: if $$i:\mathcal{A}\rightarrow\mathcal{B}$$ is an isomorphism, $a_1,...,a_n\in\mathcal{A}$, and $\varphi(x_1,...,x_n)$ is a formula, then we must have $$\mathcal{A}\models\varphi(a_1,...,a_n)\quad\iff\quad \mathcal{B}\models\varphi(i(a_1),...,i(a_n)).$$ For first-order logic this can be proved by induction on the complexity of $\varphi$, but isomorphism invariance is usually taken as part of the$^1$ definition of a logic. Thus, we have:

There is no logic according to which the successor function is definable in $\mathcal{Z}$.

Of course there are limitations to the automorphism approach. For example, the "unit distance" relation is fixed by all automorphisms of $\mathcal{Z}$, and in fact is definable over $\mathcal{Z}$ in either of the logics $\mathcal{L}_{\omega_1,\omega}$ or $\mathsf{SOL}$ (infinitary and second-order logic, respectively). So to show that the unit distance relation is not first-order definable over $\mathcal{Z}$ we have to do some work.

---

$^1$OK, this isn't really accurate: there are many different definitions out there, so what I wrote doesn't really parse. However, all the various notions that I'm aware of agree on this. For what it's worth, the one I think about most is the notion of regular logic, for which see the end of Ebbinghaus/Flum/Thomas' Mathematical Logic or the beginning of the collection Model-theoretic logics.