# Simple QE for Integer Difference Inequalities

## Language of Less-Than-Equals Over Integers

Consider language: and the theory of structure where

Lemma: This theory does not admit quantifier elimination.

Proof.

Suppose the theory admits quantifier elimination.

What is the quantifier-free formula equivalent to

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

End.

So must be expressible. Let us extend the language: consider theory in language with interpreted as on integers.

Does the theory of this structure admit quantifier elimination?

Consider quantifier-free formula equivalent to

## Extending the Language

Language:

Theory of structure where

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

In other words, we look at the language of this syntax, where 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 equivalent to?

What are conjunctions of literals equivalent to?

How do we eliminate existential quantifier?
Using and

##### Example

Prove:

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