Proving $y = x + 1$ doesn't have a quantifier-free formula in $(\mathbb{Z}, =, <)$ Assume the signature is $(\mathbb{Z}, =, <)$ with the natural interpretation, and consider whether the predicate $y = x + 1$ is representable as a quantifier-free formula in this interpretation.
First, clearly, it's representable with quantifiers: $x < y \land \forall z (x < z \rightarrow (y = z \lor y < z))$.
On the other hand, intuitively, any quantifier-free formula is just a boolean combination of atomic formulas of the form $x_i = x_j$ or $x_i < x_j$ (where $x_i, x_j$ are all either $x$ or $y$), and since any formula is by definition finite, there is just no sufficient expressive power to enumerate all the $(x, x+1)$ pairs. But how to prove this rigorously?

Quantifier-free formulas are preserved (and reflected) by embeddings. That is, if $M$ and $N$ are $L$-structures, $f\colon M\to N$ is an embedding, $\varphi(x_1,\dots,x_n)$ is a quantifier-free formula, and $a_1,\dots,a_n$ is a tuple from $M$, $$M\models \varphi(a_1,\dots,a_n) \iff N\models \varphi(f(a_1),\dots,f(a_n)).$$
This is easy to prove: it follows directly from the definition of embedding when $\varphi$ is an atomic formula, and then proceed by induction on the complexity of $\varphi$.
Now the map $x\mapsto 2x$ is an embedding $(\mathbb{Z},=,<)\to (\mathbb{Z},=,<)$, but it does not preserve the relation $y = x+1$, so this relation is not quantifier-free definable.
