This is an old revision of the document!

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 \[

  \alpha({\le}) = \{ (x,y) \mid x \le y \}

Lemma: This theory does not admit quantifier elimination.

Proof.

Suppose the theory admits quantifier elimination.

What is the quantifier-free formula equivalent to \[

  \exists x. x \le y \land x \neq y

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 \[

  \alpha(R_K) = \{ (x,y) \mid x + K \leq y \}

\] 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?

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)$

Because there are no lower or upper bounds, these formulas are $true$

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