• English only

# 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.

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?

## 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?

##### Example

Prove:

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