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.
Suppose the theory admits quantifier elimination.
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
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 | ...
Quantifier Elimination in the Extended Language
Quantifier elimination for this language is similar to Simple QE for Dense Linear Orders.
How do we eliminate existential quantifier?