  The (extended) Binary Value Principle (eBVP: $\sum_{i=1}^n x_i2^{i-1} = -k$
for $k>0$ and $x^2_i=x_i$) has received a lot of attention recently, several
lower bounds have been proved for it (Alekseev et al 2020, Alekseev 2021, Part
and Tzameret 2021). Also it has been shown (Alekseev et al 2020) that the
probabilistically verifiable Ideal Proof System (IPS) (Grochow and Pitassi
2018) together with eBVP polynomially simulates a similar semialgebraic proof
system. In this paper we consider Polynomial Calculus with the algebraic
version of Tseitin's extension rule (Ext-PC). Contrary to IPS, this is a
Cook--Reckhow proof system. We show that in this context eBVP still allows to
simulate similar semialgebraic systems. We also prove that it allows to
simulate the Square Root Rule (Grigoriev and Hirsch 2003), which is in sharp
contrast with the result of (Alekseev 2021) that shows an exponential lower
bound on the size of Ext-PC derivations of the Binary Value Principle from its
square. On the other hand, we demonstrate that eBVP probably does not help in
proving exponential lower bounds for Boolean formulas: we show that an Ext-PC
(even with the Square Root Rule) derivation of any unsatisfiable Boolean
formula in CNF from eBVP must be of exponential size.
