I've been thinking about quantifier elimination, and one thing I have gained a new appreciation for is how much of our ordinary mathematical syntax can be thought of as the "consequence" of quantifier elimination. This page lists a few examples. Modular arithmetic 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. Set operations The theory of sets has just one primitive relation, x ∈ S. But if...
