6
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Are you familiar with Ehrenfeucht-Fraisse games? $\endgroup$ – Noah Schweber Jun 11 '18 at 0:06
  • $\begingroup$ Since $x = y$ is equivalent to $\lnot (x < y) \land \lnot (y < x)$, you only need to consider $(\mathbb Z, <)$ $\endgroup$ – DanielV Jun 11 '18 at 0:51
  • 3
    $\begingroup$ 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). $\endgroup$ – DanielV Jun 11 '18 at 0:56
8
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.