# Proper definition of quantifier elimination

I study Marker book "Model Theory, An Introduction". Definition 3.1.1 on page 72 defines "theory T has quantifier elimination".

A theory $T$ has quantifier elimination if for every formula $\phi$ there is a quantifier-free formula $\psi$ such that $T \models \phi \leftrightarrow \psi$.

"$T \models \phi \leftrightarrow \psi$" is, as far as I see, actually not defined in Marker's book, but I guess with this he means $T \models \forall \vec v \; ( \phi \leftrightarrow \psi)$ where $\vec v$ is the tuple of variables in $FV( \phi ) \cup FV ( \psi )$. ($FV(\phi) =$ set of free variables of $\phi$.)

Question: Is my interpretation correct?

$\psi$ is allowed to have more free variables it seems, from above definition. Some other resources (here for example) seem to have same definition of quantifier elimination.

The above definitions don't seem to require the following: Each free variable of $\psi$ is free variable of $\phi$ (in particular, if $\phi$ is a sentence, then $\psi$ is sentence too). I saw other resource which requires it. Now this confuse me. Can someone tell me proper definition, or tell which is the most common one. For example in this resource on page 30 the definition requires it only for formulas $\psi (x_1 , \ldots, x_n )$ with "$n\geq 1$", but I don't understand what that exactly means (since sentences have no free variables so they're still of this form hence we can just leave out the $n\geq 1$ requirement).

• I don't think your interpretation is correct. Marker defines satisfaction recursively on p. 11, and his satisfaction conditions don't mention taking the universal closure of the formulas. In fact, since you want to test for quantifier elimination, it seems that the variables in $\psi$ must occur free. I'd suggest checking out Chang and Keisler's Model Theory, they explain this method in a lot of detail. – Nagase Aug 25 '14 at 5:41
• This is incomprehensible to me. Of course Marker doesn't mention taking universal closure - he leaves it undefined (as I said in my question). That was precisly my problem! What does mean "it seems that the variables in $\psi$ must occur freely"? I will check Chang/Keisler. – Aki Sakaguchi Aug 25 '14 at 18:11

Yes, your interpretation is correct. In fact writing $T \models \varphi$ for a $\mathcal L$-theory $T$ should imply that $\varphi$ is a $\mathcal L$-sentence. But model theorists are very free (no pun intended) with variables$^{[1]}$ : if $\varphi(\bar x)$ is a $\mathcal L$-formula, it certainly is a $(\mathcal L \cup \bar x)$-sentence (where every $x_i$ is now a new constant symbol). So writing $T \models \varphi(\bar x)$ for a $\mathcal L$-theory $T$ is an abuse for $\tilde T \models \varphi(\bar x)$ where $\tilde T$ is the theory $T$ viewed as a $(\mathcal L \cup \bar x)$-theory.

Now a $(\mathcal L \cup \bar x)$-structure is just an $\mathcal L$-structure with an assignation of the variables $x_i$. Then $\tilde T \models \varphi(\bar x)$ if and only if, for any $\mathcal L$-structures $\mathfrak M$ which models $T$ and for any assignation $\sigma$ of the $x_i$'s, one has $(\mathfrak M,\sigma) \models \varphi(\bar x)$. That is precisely the definition of $T \models \forall \bar x \varphi(\bar x)$.

About the "$n\geq 1$", it is a technical issue. If you allow $n=0$ on a language without constant, there as no quantifier-free sentence : you then can not find a quantifier-free sentence equivalent to $\exists x (x =x)$ for example. Requiring $n\geq 1$ forces you to consider sentences as formula of the form $\phi(y)$ : then a quantifier-free formula as $y=y$ is suitable for the previous problem.

[1] I write $\bar x$ for a tuple $(x_1,\dots,x_n)$ when I don't care about the length $n$. I the write $\varphi(\bar x)$ when the free variables of $\varphi$ are among the $x_i$'s.

• Thanks for explanation and confirmation "interpretation is correct". Now, I don't understand your "$n \geq 1$ is technical issue" explanation. First of all, do you require $FV ( \psi ) \subseteq FV ( \phi)$ or not? I see the problem when language doesn't have constant symbol. But I don't see how "requiring $n \geq 1$" solves this, because in particular all sentences are of the form $\phi ( x_1 )$. – Aki Sakaguchi Aug 25 '14 at 18:15
• @AkiSakaguchi: As you say, one can always extend the set of variables that a formula uses. Hence you can always assume that $FV(\psi) = FV(\phi)$. Requiring $n\geq 1$ solves the issue as follows: if $\phi$ is a sentence, you already know that if the language doesn't have constant symbols one can't find a qf sentence for $\phi$. But if you write it has $\phi(x_1)$, you can now find a quantifier-free $\psi(x_1)$. If the sentence is $\forall x, (x=x)$, you can eliminate the quantifiers in $(\forall x, (x=x))\land y=y$ which will yield a quantifier-free formula $\psi(y)$. – zarathustra Aug 26 '14 at 6:56

The basic semantics definitions are [see page 11] :

Definition 1.1.6 Let $\phi$ be a formula with free variables from $\overline v = (v_{i_1}, \ldots, v_{i_n})$, and let $\overline a = (a_{i_1}, \ldots, a_{i_n}) \in M^m$ [where $M$ is teh universe (or domain) of the $\mathcal L$-structure $\mathcal M$]. We inductively define $\mathcal M \vDash \phi(\overline a)$ as follows [...].

Then [page 14] :

An $\mathcal L$-theory $T$ is simply a set of $\mathcal L$-sentences.

And [page 18] :

Definition 1.2.12 Let $T$ be an $\mathcal L$-theory and $\phi$ an $\mathcal L$-sentence. We say that $\phi$ is a logical consequence of $T$ and write $T \vDash \phi$ if $\mathcal M \vDash \phi$ whenever $\mathcal M \vDash T$.

Thus, the definition at page 72 :

Definition 3.1.1 We say that a theory $T$ has quantifier elimination if for every formula $\phi$ there is a quantifier- free formula $\psi$ such that

$T \vDash \phi \leftrightarrow \psi$.

The "problem" - as you noted - is that there is no definition of logical consequence for formulae in general.

If we consider Theorem 3.1.4 :

$T \vDash \forall \overline v(\phi(\overline v) \leftrightarrow \psi (\overline v))$

We can compare it with Dirk van Dalen, Logic and Structure (5th ed - 2013), where there is an explicit "convention" in Definition 3.4.4 [page 67] :

(i) $\mathfrak A \vDash \varphi$ iff $\mathfrak A \vDash Cl(\varphi)$, [where $Cl(\varphi)$ is the universal closure of $\varphi$]

[...]

(iv) $\Gamma \vDash \varphi$ iff $(\mathfrak A \vDash \Gamma ⇒ \mathfrak A \vDash \varphi)$, where $\Gamma \cup \{ \varphi \}$ consists of sentences.

See page 98 :

Definition 4.1.4 : A theory $T$ is a collection of sentences with the property $T \vdash \varphi ⇒ \varphi \in T$.

Finally, see the brief treatment of quantifier elimination [page 121-on] :

Since $T$ admits quantifier elimination, there is a quantifier-free $\psi(x_1,\ldots, x_n)$ such that $T \vdash \varphi \leftrightarrow \psi$.

Note that in Marker's book intro [page 4] there is a reference to Joseph Shoenfield, Mathematical Logic (1968) as a "background in mathematical logic".

In Shoenfield's book [page 83] we have :

We say that [a formula] $A$ is equivalent to $B$ in [a theory] $T$ if $\vdash_T A \leftrightarrow B$. We say that $T$ admits elimination of quantifiers if every formula in $T$ is equivalent in $T$ to an open formula.

we introduced the notion of a sentence $\varphi$ being a consequence of a set $\Sigma$ of sentences, in symbols $\Sigma \vDash \varphi$. What meaning shall we give to $\Sigma \vDash \varphi$ if $\varphi$ is a formula? We shall say that a formula $\varphi (v_0 \ldots v_n)$ is a consequence of $\Sigma$, symbolically $\Sigma \vDash \varphi$, iff for every model $\mathfrak A$ of $\Sigma$ and every sequence $a_0,\ldots, a_n \in A$, $a_0,\ldots, a_n$ satisfies $\varphi$. It follows that the formula $\varphi(v_0 \ldots v_n)$ is a consequence of $\Sigma$ if and only if the sentence $(\forall v_0 \ldots v_n) \varphi(v_0 \ldots v_n)$ is a consequence of $\Sigma$.
We say that two formulas $\varphi, \psi$ are $\Sigma$-equivalent iff $\Sigma \vDash \varphi \leftrightarrow \psi$.
THEOREM 1.5.3. Every formula $\varphi$ is $\Delta$-equivalent to an open formula $\psi$ [where $\Delta$ is the theory of dense simple order without endpoints].