= Morleyization
{c}
{title2=$P_\phi(\vec x)\leftrightarrow\phi(\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>.
Back to article page
