Revised: September 20, 2025
Published: June 21, 2026
Abstract: [Plain Text Version]
A major proof complexity problem is to prove a superpolynomial lower bound on the length of Frege proofs of arbitrary depth. A more difficult question is to prove an Extended Frege lower bound. Surprisingly, proving such bounds turns out to be much easier in the algebraic setting. In this paper, we study a proof system that can efficiently simulate Extended Frege: an extension of the Polynomial Calculus proof system where we can take a square root and introduce new variables that are equivalent to algebraic circuits of arbitrary depth. We prove that an instance of the subset-sum principle, the binary value principle $1 + x_1 + 2 x_2 + \ldots + 2^{n - 1} x_n = 0$ ($\mathsf{BVP}_n$), requires refutations of exponential bit size over $\Q$ in this system.
Part and Tzameret (ITCS'20) proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations) refutations of $\mathsf{BVP}_n\,.$ We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of $\mathsf{BVP}_n\,.$
---------------
A preliminary version of this paper appeared in the Proceedings of the 36th Conference on Computational Complexity (CCC'21).
Licensed under a Creative Commons Attribution License (CC-BY)