= Solution
Add a <predicate symbol> $P_\theta$ for each $L$-formula $\theta(\vec x)$, of arity equal to its displayed free-variable <tuple>. Let $T^+$ consist of $T$ together with all defining axioms
$$
\forall\vec x\ (P_\theta(\vec x)\leftrightarrow\theta(\vec x)).
$$
Every <first-order model> of $T$ has a unique such expansion, interpreting the new <predicate symbols> by their defining <sets>. Conversely the reduct of every <first-order model> of $T^+$ satisfies $T$.
Given an arbitrary $L^+$-formula $\psi(\vec x)$, replace each new atomic <predicate symbol> by its original $L$-definition, renaming <bound variables> to avoid capture. This produces an $L$-formula $\psi^-(\vec x)$ with
$$
T^+\models\forall\vec x\ (\psi(\vec x)\leftrightarrow\psi^-(\vec x)).
$$
The defining axiom for that particular <logical formula> now gives an atomic replacement:
$$
\boxed{T^+\models\forall\vec x\ (\psi(\vec x)\leftrightarrow P_{\psi^-}(\vec x)).}
$$
Thus the expanded <first-order theory> eliminates <quantifiers>. For a <first-order sentence>, the same translation is an $L$-sentence, decided by completeness of $T$; hence every expanded <first-order sentence> is decided and $T^+$ is complete. Empty free-variable <tuples> can be handled by zero-ary <predicate symbols>, or by the usual <logical truth> and falsity constants. This definitional expansion is called <Morleyization>.
Back to article page
