I need to prove that every theory eliminates quantifiers in an appropriate definitional expansion. For this, consider: let $T$ be a theory in language $L$. Consider the following expansion of the language: for each $L$- formula $\varphi(\bar x)$ add a relation $R_\varphi$, whose arity is the length of $\bar x$. Consider the theory $T'$ obtained by adding, for each $L$-formula $\varphi(\bar x)$, the axiom $\forall \bar x (\varphi (\bar x)\leftrightarrow R_\varphi(\bar x))$ to $T$. Prove that:

  1. Each model of $T$ has a unique expansion to a model of $T'$.

  2. If $\varphi$ is an $L$-sentence and $T'\models \varphi$ then $T\models \varphi$.

  3. For every $\varphi (\bar x ) \in L'$ there is $\psi(\bar x) \in L$ such that $T' \models \varphi (\bar x) \leftrightarrow \psi(\bar x)$.

  4. $T'$ has quantifier elimination.

So, for the first item, I have to do two things, one is to show that there is an expansion and the other that it is unique. I guess that to prove that it is unique I need to take 2 "different" expansions and show that they are the same. I don't really know how to properly start writing this, so I would appreciate your input.

For the second one... it seems "evident", but I don't know how to justify it. Assume $T' \models \varphi$, so $T' \models \forall \bar x (\varphi (\bar x)\leftrightarrow R_\varphi(\bar x))$ (can i say that?), I don't really know how to go from here.

I'm really at lost about how to continue, and I would really appreciate your help explaining me how to go about this.


2 Answers 2


For 1): Start with some $\mathcal{M}\models T$ where $M$ is the underlying set of the model $\mathcal{M}$. Given an $L$-formula $\varphi(x_1, x_2,\ldots, x_n)$ (with $n$ free variables) let $R_\varphi^{\mathcal{M}^\prime}=\{(a_1,a_2,\ldots, a_n)\in M^n: \mathcal{M}\models\varphi(a_1, a_2,\ldots, a_n)\}$. Do this for each $L$-formula $\varphi$, and then extend $\mathcal{M}$ by adding to it the sets $R_\varphi^{\mathcal{M}^\prime}$, and call this new model $\mathcal{M}^\prime$. Then $\mathcal{M}^\prime$ is an $L^\prime$ structure by interpreting the symbols of $L$ the same way $\mathcal{M}$ interpreted them, and interpreting the new symbols of the form $R_\varphi$ as $R_\varphi^{\mathcal{M}^\prime}$. Then $\mathcal{M}^\prime$ is a model for $T^\prime$ (not too hard to show).

For uniqueness, it is enough to show that $R_\varphi^\mathcal{B}=R_\varphi^{\mathcal{M}^\prime}$ whenever $\mathcal{B}$ is an expansion of $\mathcal{M}$ which models $T^\prime$. So taking an $L$-formula $\varphi(x_1, x_2,\ldots, x_n)$ (with $n$ free variables), we have $(a_1, a_2, \ldots, a_n)\in R_\varphi^{\mathcal{M}^\prime}$ iff $\mathcal{M}^\prime\models R_\varphi(a_1, a_2, \ldots, a_n)$ iff $\mathcal{M}^\prime\models \varphi(a_1, a_2, \ldots, a_n)$ iff $\mathcal{M}\models \varphi(a_1, a_2, \ldots, a_n)$ iff $\mathcal{B}\models\varphi(a_1, a_2, \ldots, a_n)$ iff $\mathcal{B}\models R_\varphi(a_1, a_2, \ldots, a_n)$ iff $(a_1, a_2, \ldots, a_n)\in R_\varphi^\mathcal{B}$.

  • $\begingroup$ Thank you for your help, this is much clearer! $\endgroup$
    – Sara
    May 9, 2015 at 9:51
  1. is answered by Sam.

  2. follows from 1. In fact, if $T\not\models\varphi$ then there is a $M\models T\cup\{\neg\varphi\}$, hence an expansion $M'\models T'$ which clearly models $\neg\varphi$. (The converse implication follows by the same argument with $\neg\varphi$ for $\varphi$.)

  3. is true by definition for atomic functions. Then, by induction, it holds for all formulas.

  4. Every $L$-formula is equivalent over $T'$ to an atomic (hence quantifier-free) $L'$-formula. By 3, the same holds for all $L'$-formulas.

  • $\begingroup$ Thank you very much for your help, 1, 2 and 3 are clear now, but I'm still a bit confused about how to get 4. I get that what I'm doing is pretty much transforming all of my formulas into relations, hence making them all atomic, but I am having some issues expressing it formally, I would appreciate your advice about how to do this. $\endgroup$
    – Sara
    May 9, 2015 at 9:58
  • $\begingroup$ Primo Petri's answer to 4 is perhaps a bit misleading: by 3, every $L'$ formula $\phi(\overline{x})$ is equivalent over $T'$ to an $L$-formula $\psi(\overline{x})$, but then $\psi(\overline{x})$ is equivalent over $T'$ to the atomic formula $R_{\psi}(\overline{x})$. $\endgroup$
    – Rob Arthan
    May 9, 2015 at 16:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .