Some Surprising Quantifier Elimination Operators

The mod operation, as in x % 3, is necessary to eliminate existentials like:

∃ x, y = 3 x + 2

Here the quantifier elimination results in y % 3 = 2. Moreover, the theory has quantifier elimination once you add modulus, which distinguishes this existential as worth naming.

The theory of sets has just one primitive relation, x ∈ S. But if you add quantifiers you get equations like:

∃ x, x ∈ S /\ x ∉ T

This quantifier-eliminates to ¬ (S ⊆ T). In other words, set operations eliminate quantifiers over set members. Moreover, once you add the boolean algebra operations on sets, this theory has quantifier elimination.

I struggled for a while to understand why the theory of nonlinear real arithmetic always had inequalities instead of simple equalities. Eventually I realized: eliminate this quantifier, and you get x ≥ 0.

∃ y, y^2 = x

So the ordering on real numbers is actually a consequence of quantifier elimination. In a sense, that's why you don't have an order on complex numbers, because they are algebraically complete so quantifier elimination exists without adding new relations. Anyway, order then gives you quantifier elimination via cylindrical algebra decomposition.

The theory of linear differentially closed fields of characteristic 0 describes complex functions which you can add or differentiate. In this theory, eliminate this quantifier to get the exponential function:

∃ f, ∂ f = f

Moreover, once you do that the theory now has quantifier elimination (using the usual matrix Jordan block thing) so again the exponential function is distinguished.