The Dual of Quantifier Elimination: Boolean Elimination over C and R
Matthew Frank

TL;DR
This paper introduces a dual approach to quantifier elimination in algebraic geometry, providing uniform normal forms with minimal quantifiers for Boolean combinations of polynomial equations over complex and real fields.
Contribution
It establishes the existence of simple, uniform normal forms with minimal quantifiers for Boolean combinations of polynomial equalities and inequalities, extending classical quantifier elimination.
Findings
Normal forms with one existential and one universal quantifier over C and R.
No purely existential or universal normal form is possible over C.
Results apply to constructible sets, entire functions, and functional languages over infinite fields.
Abstract
We show that every finite Boolean combination of polynomial equalities and inequalities in C^n admits two uniform normal forms: an form and a form, each using a single polynomial equation. Both forms use only one existentially quantified variable and one universally quantified variable. Optimality results demonstrate that no purely existential or universal normal form is possible over C. These results extend to sets constructible from entire functions, and to quantifier-free formulas in functional languages over infinite fields of characteristic 0. A corollary shows Zilber's conjecture on quasiminimality equivalent to its subcase quantifying a single equation. Over R and Q, similar results hold, including a singly-quantified form for Boolean combinations of equations and inequations, an form for R established by prior methods,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPolynomial and algebraic computation · Complexity and Algorithms in Graphs · Formal Methods in Verification
