Existential common-substructure test for quantifier elimination

ID: existential-common-substructure-test-for-quantifier-elimination

For a first-order theory , suppose every existential quantifier-free formula over a common substructure has a witness in either of two -models exactly when it has one in the other. Then 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.

New to topics? Read the docs here!