The Surprising Power Of Constant Depth Algebraic Proofs

A major open problem in proof complexity is to prove superpolynomial lower bounds for AC(empty set) [p] -Frege proofs. This system is the analog of AC(empty set) [p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years ([28, 30]), there are no significant lower bounds for AC(empty set) [p]-Frege. Significant and extensive degree lower bounds have been obtained for a variety of subsystems of AC(empty set) [p]-Frege, including Nullstellensatz ([3]), Polynomial Calculus ([9]), and SOS ([14]). However to date there has been no progress on AC(empty set) [p]-Frege lower bounds.In this paper we study constant-depth extensions of the Polynomial Calculus [13]. We show that these extensions are much more powerful than was previously known. Our main result is that small depth (<= 43) Polynomial Calculus (over a sufficiently large field) can polynomially effectively simulate all of the well-studied semialgebraic proof systems: Cutting Planes, Sherali-Adams, Sum-of-Squares (SOS), and Positivstellensatz Calculus (Dynamic SOS). Additionally, they can also quasi-polynomially effectively simulate AC(empty set) [q] -Frege for any prime q independent of the characteristic of the underlying field. They can also effectively simulate TCempty set-Frege if the depth is allowed to grow proportionally. Thus, proving strong lower bounds for constant-depth extensions of Polynomial Calculus would not only give lower bounds for AC(empty set )[p]-Frege, but also for systems as strong as TCempty set-Frege.