Algebraically prime extension test for quantifier elimination

ID: algebraically-prime-extension-test-for-quantifier-elimination

If has algebraically prime models and every inclusion between models of is a simple closure, then has quantifier elimination. For a common base , embed its algebraically prime extension into both models. Simple closure transfers a witness into that extension; the second embedding transfers it to the other model.

New to topics? Read the docs here!