Morleyization ($P_{\varphi }(\vec{x})\leftrightarrow \varphi (\vec{x})$)

Morleyization adds a predicate symbol for each first-order formula and an axiom equating that predicate symbol with its defining logical formula. Every original first-order model has a unique expansion. Translating an expanded logical formula back to the original first-order language and then using its named predicate symbol gives quantifier elimination. Completeness of the original first-order theory implies completeness of the expanded first-order theory.