Simple QE for Integer Difference Inequalities

Language of Less-Than-Equals Over Integers

Consider language: ${\cal L} = \{ {\le} \}$ and the theory of structure $I = (\mathbb{Z},\alpha)$ where

$\begin{equation*} \alpha({\le}) = \{ (x,y) \mid x \le y \} \end{equation*}$

Lemma: This theory does not admit quantifier elimination.

Proof.

Suppose the theory admits quantifier elimination.

What is the quantifier-free formula equivalent to

$\begin{equation*} \exists x. x \le y \land x \neq y \end{equation*}$

It is formula with one free variable, $y$ . So it must be built out of atomic formulas $y \leq y$ and $y=y$ , and is therefore it is either always true or always false, regardless of the value of $y$ . It thus cannot be equivalent to the above formula.

End.

So $<$ must be expressible. Let us extend the language: consider theory in language ${\cal L} = \{ \le, < \}$ with $<$ interpreted as $<$ on integers.

Does the theory of this structure admit quantifier elimination?

Consider quantifier-free formula $F(x,z)$ equivalent to $\exists y_1. \ldots \exists y_n.\ x < y_1 < y_2 < \ldots < y_n < z$

Extending the Language

Language: ${\cal L} = \{ R_K \mid K \in \mathbb{Z} \}$

Theory of structure $I = (\mathbb{Z},\alpha)$ where

$\begin{equation*} \alpha(R_K) = \{ (x,y) \mid x + K \leq y \} \end{equation*}$

Note that $R_0$ is the less-than-equal relation on integers.

In other words, we look at the language of this syntax, where $V$ is the set of variables:

F ::= A | (F&F) | (F|F) | ~F | ALL V.F | EX V.F
A ::= v=v | v + K ≤ v | true | false
K ::= ... -2 | -1 | 0 | 1 | 2 | ...

Equality is expressed by $x + 0 \leq y \wedge y + 0 \leq x$

Quantifier Elimination in the Extended Language

Quantifier elimination for this language is similar to Simple QE for Dense Linear Orders.

What is $\lnot (x + K \le y)$ equivalent to?
$y < x + K$
$y + 1 \le x + K$
$y + (1-K) \le x$

What are conjunctions of literals equivalent to?

$\exists y. \bigwedge_{i=1}^n x_i+K_i \le y \land \bigwedge_{j=1}^m y + L_j \le z_j$

How do we eliminate existential quantifier?
Using $x_i + K_1 \le y$ and $y \le z_j - L_j$

$\bigwedge_{i,j} x_i + K_i \le z_j - L_j$
$\bigwedge_{i,j} x_i + (K_i + L_j) \le z_j$

Example

Prove:

$\forall y \exists x . x \leq y \wedge x \neq y$

$\exists x . x \leq y \wedge (x < y \vee y < x)$
$\exists x . x \leq y \wedge (x + 1 \leq y \vee y + 1 \leq x)$
$(\exists x . x \leq y \wedge x + 1 \leq y) \vee (\exists x . x \leq y \wedge y + 1 \leq x)$
$true \vee false$
$true$

If we apply this technique to a closed formula in this theory, what formulas do we obtain as a result?