LARA

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.

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?

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

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?

What are conjunctions of literals equivalent to?

How do we eliminate existential quantifier?

Example

Prove:

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

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