= Existential common-substructure test for quantifier elimination
= QET1
{c}
{synonym}
For a <first-order theory> $T$, suppose every existential <quantifier-free formula> over a common <substructure> has a witness in either of two $T$-models exactly when it has one in the other. Then $T$ has <quantifier elimination>. One may test a single quantified variable, since elimination of these formulas inductively eliminates all quantifiers. A language with a constant avoids empty-generated-substructure and quantifier-free-sentence conventions.
Back to article page
