Abstract
A major proof complexity problem is to prove a superpolynomial lower bound on the length of Frege proofs of arbitrary depth. A more general 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 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 arbitrary depth algebraic circuits. We prove that an instance of the subsetsum principle, the binary value principle 1 + x₁ + 2 x₂ + … + 2^{n1} x_n = 0 (BVP_n), requires refutations of exponential bit size over ℚ in this system.
Part and Tzameret [Fedor Part and Iddo Tzameret, 2020] proved an exponential lower bound on the size of ResLin (Resolution over linear equations [Ran Raz and Iddo Tzameret, 2008]) refutations of BVP_n. We show that our system psimulates ResLin and thus we get an alternative exponential lower bound for the size of ResLin refutations of BVP_n.
BibTeX  Entry
@InProceedings{alekseev:LIPIcs.CCC.2021.21,
author = {Alekseev, Yaroslav},
title = {{A Lower Bound for Polynomial Calculus with Extension Rule}},
booktitle = {36th Computational Complexity Conference (CCC 2021)},
pages = {21:121:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771931},
ISSN = {18688969},
year = {2021},
volume = {200},
editor = {Kabanets, Valentine},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14295},
URN = {urn:nbn:de:0030drops142959},
doi = {10.4230/LIPIcs.CCC.2021.21},
annote = {Keywords: proof complexity, algebraic proofs, polynomial calculus}
}
Keywords: 

proof complexity, algebraic proofs, polynomial calculus 
Collection: 

36th Computational Complexity Conference (CCC 2021) 
Issue Date: 

2021 
Date of publication: 

08.07.2021 