Quantifier Elimination in Model Theory – Formula with Free Variables

logicmodel-theoryquantifier-elimination

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.

Best Answer

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))$.

Related Question