The Power of the Binary Value Principle

The (extended) Binary Value Principle(formula presented) and in the presence of has received a lot of attention recently, several lower bounds have been proved for it [1, 2, 10]. It has been shown [2] that the probabilistically verifiable Ideal Proof System [8] together with polynomially simulates a similar semialgebraic proof system. In this paper we consider Polynomial Calculus with the algebraic version of Tseitin’s extension rule(formula presented), this is a Cook–Reckhow proof system. We show that in this context still allows to simulate similar semialgebraic systems. We also prove that it allows to simulate the Square Root Rule [6] in a sharp contrast to the result of [1] that shows an exponential lower bound on the size of (formula presented) from its square. On the other hand, we demonstrate that probably does not help in proving exponential lower bounds for Boolean formulas: we show that an (formula presented) (even with the Square Root Rule) derivation of any unsatisfiable Boolean formula in CNF from must be of exponential size.