# Every theory eliminates quantifiers in an appropriate definitional expansion?

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.

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

• Thank you for your help, this is much clearer! – Sara May 9 '15 at 9:51
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$.)
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.
• 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})$. – Rob Arthan May 9 '15 at 16:09