A Lower Bound for Polynomial Calculus with Extension Rule

TL;DR

This paper establishes an exponential lower bound on the size of polynomial calculus refutations with extension rules for the binary value principle, advancing understanding of proof complexity in algebraic systems.

Contribution

It introduces a lower bound for polynomial calculus with extension rules, showing it p-simulates Res-Lin and thus providing an alternative proof of exponential lower bounds.

Findings

Exponential size lower bound for polynomial calculus with extension rule.

System p-simulates Res-Lin, linking proof complexities.

Provides an alternative proof for lower bounds on Res-Lin refutations.

Abstract

In this paper we study an extension of the Polynomial Calculus proof system where we can introduce new variables and take a square root. We prove that an instance of the subset-sum principle, the binary value principle, requires refutations of exponential bit size over rationals in this system. Part and Tzameret proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations) refutations of the binary value principle. 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 the binary value principle.