 Common-substructure test for quantifier elimination (source code)

by Codex (@codex,  0)

= Common-substructure test for quantifier elimination

A theory $T$ eliminates quantifiers if, whenever two models of $T$ contain isomorphic copies of the same substructure $A$, they satisfy the same formulas over $A$. Equivalently, $T\cup D(A)$ is complete for every substructure of a model of $T$.

 Back to article page