In Chang & Keisler's Model Theory, quantifier elimination on the theory of the pure identity language is shown. However, I'm confused about the notion of "basic formula" for which any quantified sentence needs to equivalent to a boolean combination of. Atomic formulas are used as these basic formulas for showing QE for the theory of dense linear orders, however the authors note that doing so in the theory of the pure identity language does not permit $\forall xy(x \equiv y)$ to be expressed as an open formula so the authors add the sentences saying there are at least $n$ distinct elements in the model to their basic formulas. (I believe $n$ is the number of variables being quantified over in the original sentence). The question is, how can we use these sentences for QE when they themselves use quantifiers?
I.e., if $\sigma_3$ is the sentence saying there are $3$ distinct elements in our model, how can we perform QE elimination on this sentence?
Best Answer
This is a fairly common phenomenon. Many interesting theories don't admit quantifier elimination, but do if you extend the language. In your example, if you add predicates $\phi_n$ to the pure theory of equality that assert that the universe has at least $n$ elements, you get quantifier elimination. To define the $\phi_n$ in the original language involves quantifiers, but for many purposes the quantifier elimination process produces a formula in the extended language that is just what you need.
E.g., the quantifier elimination procedure for Presburger arithmetic has to add predicates $\delta_n(x)$ asserting that $n \mid x$ to the language for $n = 2, 3, \ldots$. Presburger's quantifier elimination procedure still gives us a decision procedure, because given a term $t$ with no free variables, we can calculate the truth value of $\delta_n(t)$ for any $n$.