Upper and Lower bounds for Polynomial Calculus with extension variables

A major open problem in proof complexity is to prove superpolynomial lower bounds for AC0[p]-Frege proofs. This system is the analog of AC0[p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years ([Raz87, Smo87]), there are no significant lower bounds for AC0[p]-Frege. Significant and extensive degree lower bounds have been obtained for a variety of subsystems of AC0[p]- Frege, including Nullstellensatz ([BIK+94]), Polynomial Calculus ([CEI96]), and SOS ([GV01]). However to date there has been no progress on AC0[p]-Frege lower bounds.In the first part of this thesis, we study constant-depth extensions of the Polynomial Calculus [GH03]. 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 AC0[q]-Frege for any prime q independent of the characteristic of the underlying field. They can also effectively simulate TC0-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 AC0[p]-Frege, but also for systems as strong as TC0-Frege. In the second part of this thesis, we deal with the flip side of proving new lower bounds for these systems. In this direction, we extend the recent lower bounds of Sokolov [Sok20] for Polynomial Calculus over {±1} variables to show for every prime p > 0, every n > 0 and κ = O(log n) the existence of an unsatisfiable system of polynomial equations over O(n log n) variables of degree O(logn) such that any Polynomial Calculus refutation over F_p with M extension variables, each depending on at most κ original variables requires size exp?Ω(n2/(κ22κ(M + nlog(n))))