Modeling a formula with free variables for quantifier elimination, i.e. $\mathfrak{M} \models \phi (x) \leftrightarrow \psi (x)$

Question

I am an undergrad doing an independent study with a professor on model theory using David Marker's Model Theory : An Introduction. I am new to the subject so this question may be naïve or misguided.

I am trying to understand the chapter on quantifier elimination. As I understand it, saying a theory or a structure models a formula doesn't make sense with free variable $x=(x_1,\dots, x_n)$, i.e. $\mathfrak{M} \models \gamma{({x})} $ is not a meaningful statement. That said, a different text I read says (if I understand it correctly) that $\mathfrak{M} \models \gamma{({x})} $ if every assignment function for the variable $x$ renders the above true, which is to say $\mathfrak{M} \models \gamma{({x})} \iff \mathfrak{M} \models \forall y\ \gamma (y) $. This does not make sense to me as it seems to imply every theory has quantifier elimination, because if we can eliminate the universal quantifier in any sentence, by its equivalence to $\neg \exists x \neg$, it would seem we could eliminate quantifiers in anything. On page 73 Marker writes as part of the proof that DLO, the theory of dense linear orders, has quantifier elimination:

$\mathbb{Q} \models \phi (\bar{x}) \rightarrow \psi_\phi (\bar{x})$

and I want to understand how to interpret such statements. Thank you.

Answer 1

A theory $T$ eliminates quantifiers if, for every formula $\varphi(x)$ (with free variables from $x = (x_1,\dots,x_n)$, where $n\geq 0$), there exists a quantifier-free formula $\psi(x)$ (with free variables from $x$) such that $T\models \forall x\, (\varphi(x)\leftrightarrow \psi(x))$.

It is a common convention to treat free variables on the right-hand-side of $\models$ as implicitly universally quantified. Under this convention, $M\models \varphi(x)$ if and only if $M\models \forall x\, \varphi(x)$, and $T\models \varphi(x)$ if and only if $T\models \forall x\, \varphi(x)$.

But even if we adopt this convention, we do not automatically get quantifier elimination. Note that $T\models \varphi(x)$ if and only if $T\models \forall x\, \varphi(x)$ does not imply $T\models \forall x\, (\varphi(x)\leftrightarrow \forall x\, \varphi(x))$.

Answer 2

Some authors adopt the convention that ${\cal M} \models \gamma(x_1, \ldots, x_n)$ is allowed when $\gamma(x_1, \ldots, x_n)$ has free variables $x_1, \ldots, x_n$ and serves as a short-hand for ${\cal M} \models \forall x_1\ldots\forall x_n\gamma(x_1, \ldots, x_n)$. (And some authors allow it and take it as a short-hand for ${\cal M} \models \exists x_1\ldots\forall x_n\gamma(x_1, \ldots, x_n)$ - caveat emptor). These conventions about $\models$ don't have anything to do with quantifier elimination, which is about the existence of quantifier-free equivalents for formulas.