# 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?

• Are you familiar with Ehrenfeucht-Fraisse games? – Noah Schweber Jun 11 '18 at 0:06
• Since $x = y$ is equivalent to $\lnot (x < y) \land \lnot (y < x)$, you only need to consider $(\mathbb Z, <)$ – DanielV Jun 11 '18 at 0:51
• Also since you only have 2 object variables $x$ and $y$, then you only have 2 propositional terms $x < y$ and $y < x$, and there are only 16 unique ways to create a propositional formula out of them (16 binary gates). – DanielV Jun 11 '18 at 0:56

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.