Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Matthew Frank

TL;DR

The paper establishes a dual to classical quantifier elimination: any finite Boolean combination of polynomial equations and inequalities can be represented by a single polynomial equation under a minimal two-block quantifier prefix, with explicit constructions and linear degree bounds over $\mathbb{C}$. It shows that over $\mathbb{C}$ one can use either $\exists a \forall b$ or $\forall a \exists b$ to encode the Boolean structure, and proves that purely existential or universal single-equation forms are impossible, demonstrating optimal quantifier alternation. The results extend to $\mathbb{R}$ and $\mathbb{Q}$ with analogous forms (e.g., $\exists$ or $\exists^d$ and $\forall\exists$ variants) and leverage tools like Lagrange interpolation and sum-of-squares encodings. This Boolean elimination perspective provides a practical and uniform framework with potential applications to model theory and semialgebraic set analysis, offering a contrasting approach to QE by trading propositional complexity for a compact quantifier prefix.

Abstract

We show that every finite Boolean combination of polynomial equalities and inequalities in C^n admits two uniform normal forms: an $\exists\forall$ form and a $\forall\exists$ form, each using a single polynomial equation. Both forms have one existentially quantified variable and one universally quantified variable; regardless of the complexity of the original formula, no longer quantifier blocks are needed. The constructions are explicit and have linear degree bounds. Optimality results demonstrate that no purely existential or universal normal form is possible over C. Over R, similar normal forms exist, including a singly-quantified $\exists$ form for Boolean combinations of equations and inequations, and $\exists^d$ and $\forall\exists$ forms for Boolean combinations involving order inequalities. Prior results establish the existence of a $\exists$ normal form for R by other methods. Finally, similar forms exist over Q as well. These results may be viewed as a dual to classical quantifier elimination: instead of removing quantifiers at the cost of increased Boolean complexity, they remove Boolean structure at the cost of a short, fixed quantifier prefix.

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

TL;DR

The paper establishes a dual to classical quantifier elimination: any finite Boolean combination of polynomial equations and inequalities can be represented by a single polynomial equation under a minimal two-block quantifier prefix, with explicit constructions and linear degree bounds over . It shows that over one can use either or to encode the Boolean structure, and proves that purely existential or universal single-equation forms are impossible, demonstrating optimal quantifier alternation. The results extend to and with analogous forms (e.g., or and variants) and leverage tools like Lagrange interpolation and sum-of-squares encodings. This Boolean elimination perspective provides a practical and uniform framework with potential applications to model theory and semialgebraic set analysis, offering a contrasting approach to QE by trading propositional complexity for a compact quantifier prefix.

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 have one existentially quantified variable and one universally quantified variable; regardless of the complexity of the original formula, no longer quantifier blocks are needed. The constructions are explicit and have linear degree bounds. Optimality results demonstrate that no purely existential or universal normal form is possible over C. Over R, similar normal forms exist, including a singly-quantified form for Boolean combinations of equations and inequations, and and forms for Boolean combinations involving order inequalities. Prior results establish the existence of a normal form for R by other methods. Finally, similar forms exist over Q as well. These results may be viewed as a dual to classical quantifier elimination: instead of removing quantifiers at the cost of increased Boolean complexity, they remove Boolean structure at the cost of a short, fixed quantifier prefix.

Paper Structure

This paper contains 10 sections, 16 theorems, 38 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Context
  3. Normalizing to $EA$ over $C$
  4. Normalizing to $AE$ over $C$
  5. Optimality: the quantifier prefixes cannot be shortened over $C$
  6. Extending the results on equations from $C$ to $R$
  7. Normalizing to $E^d$ and $AE$ over $R$
  8. Single-quantifier $E$ forms over $R$
  9. Normal forms over $Q$
  10. Conclusion

Key Result

Theorem 1.1

[Boolean Elimination over $C$] Let $\varphi(x)$ be any Boolean combination of polynomial equations and inequations in variables $x\in\mathbb{C}^n$. Then there are polynomials such that for all $x\in\mathbb{C}^n$,

Figures (1)

  • Figure 1: Graph for a simple version of Pecker's polynomial

Theorems & Definitions (20)

  • Theorem 1.1
  • Lemma 3.1
  • Lemma 3.2
  • Lemma 3.3
  • Theorem 4.1
  • Theorem 5.1
  • Lemma 6.1
  • Corollary 6.1
  • Theorem 6.1
  • proof
  • ...and 10 more