I Need Help Understanding Quantifier Elimination

The intuition is that, in a model with quantifier elimination, the definable sets are likely to be extremely simple.

The easiest example is the theory of dense linear orderings without endpoints. A set definable by a quantifier-free formula will consist of a finite union of individual points and intervals, by inspection of the formula. Because each model $M$ has quantifier elimination (in a signature with a constant for each element), every definable set will be of that simple form. If we do not add constants for elements, the quantifier-free formulas are all equivalent to $\top$ or to $\bot$, and so there are only two definable sets, $|M|$ and $\emptyset$. This also shows - syntactically - that the theory of dense linear orderings without endpoints is complete.

Quantifier elimination is also helpful for proving that theories are decidable. If the quantifier elimination procedure is effective - meaning there is a computable function mapping arbitrary formulas to quantifier-free equivalent formulas - this often gives a proof that the theory is decidable. This is because the function would have to map arbitrary sentences to equivalent quantifier-free sentences, and in many cases the truth of quantifier-free sentences can be decided algorithmically. This is one way to prove the decidability of the theory of the real numbers as an ordered field, for example: there is effective quantifier elimination, and truth of quantifier-free sentences can be decided algorithmically.

Suppose we have a class $K$ of models. That we have quantifier elimination for $K$ means that for every formula $\varphi(x)$ there is a quantifier-free formula $\psi(x,y)$ such that for every $M\in K$ we have $M\models \varphi(x)\leftrightarrow \psi(x,y)$ (where $x,y$ are tuples of finite length).

It does not, however, mean that the theory itself can be expressed without quantifiers, even if we assume that $K$ is an elementary class. This is not the case for the commonly known complete theories with quantifier elimination, such as $DLO_0$ (dense linear orderings without endpoints), $ACF_p$ (algebraically closed fields of characteristic $p$) or $RCF$ (real closed fields with $\leq$). A theory which has q.e. and is axiomatisable without quantifiers will likely be rather dull, though I don't feel like exploring how dull exactly it would be.

The process in the theorem is as follows:

1. We have a set of formulas $\Phi$ we want to show is an elimination set. This means that any first-order formula in $L$ is equivalent to a boolean combination of elements of $\Phi$.
2. Every first order formula comes from atomic formulas in a finite sequence of alternating two operations: taking a boolean combination and prefixing an existential quantifier. We can do induction with respect to complexity of formulas defined as the length of this finite sequence.
3. So, if $\Phi$ contains an atomic formula (base case of induction), and every boolean combination of formulas in $\Phi$ prefixed by an existential quantifier is equivalent to a boolean combination of formulas without said quantifier then by induction we have...?