Proper definition of quantifier elimination

Question

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

Answer 1

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.

Answer 2

Some comments about your critique regarding some "imperfections" in Marker's treatment.

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 have exactly your interpretation.

---

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

---

Addendum

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.

---

2nd Addendum

Regarding C.C.Chang & H.Jerome Keisler, Model Theory (3rd ed, 1990), they are in the "mainstream" tradition of model theory, "restricting" the basic semantics definition of theory and logical consequence to sentences.

But [see page 50] they introduce the topic of quantifier elimination in this way :

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

Thus, they prove [page 52] :

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].