[Proof Complexity] a new preprint

[Edward A. Hirsch]

Dear Colleagues,

Here is our new preprint:
     http://arxiv.org/abs/2210.17429
It concerns algebraic systems with Tseitin's extension rule,
the Square Root Rule, and the Binary Value Principle.
Also a lower bound on deriving any CNF from BVP is proved.

The abstract is below.
Comments are welcome!

Best regards,
Edward
--
Edward A. Hirsch
Technion
%----------------------------------------------------
The power of the Binary Value Principle
Yaroslav Alekseev, Edward A. Hirsch

The (extended) Binary Value Principle (eBVP:  \sum x_i2^{i-1} = -k for
k>0 and x_i^2=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 absolutely
unclear in the context of ordinary Polynomial Calculus. On the other
hand, we demonstrate that eBVP probably does not help in proving
exponential lower bounds for Boolean tautologies: we show that an
Ext-PC (even with the Square Root Rule) derivation of any such
tautology from eBVP must be of exponential size.
%----------------------------------------------------