Axioms Polynomially Simulate Nullstellensatz

Title: Axioms Polynomially Simulate Nullstellensatz

Abstract: This research article explores the relationship between constant-depth Frege systems with counting axioms and the Nullstellensatz system. The authors show that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo n. This allows them to establish a size separation between Nullstellensatz and polynomial calculus refutations, which is a significant achievement in the field of propositional proof systems. Additionally, the authors introduce a new definition of reducibility from formulas to systems of polynomials, which is particularly useful for translating formulas into systems of polynomials.

Main Research Question: Can constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo n?

Methodology: The authors use a combination of algebraic and combinatorial methods to prove their results. They introduce a new definition of reducibility from formulas to systems of polynomials, which allows them to show that if a formula has a small reduction to a set of polynomials with a small Nullstellensatz refutation, then the formula has a small refutation in constant-depth Frege with counting axioms.

Results: The main result of the paper is the proof that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo n. This allows the authors to infer size lower bounds for Nullstellensatz refutations from size lower bounds for constant-depth Frege with counting axioms proofs.

Implications: The results of this paper have important implications for the field of propositional proof systems. The size separation between Nullstellensatz and polynomial calculus refutations establishes a new lower bound for the complexity of propositional proofs. Additionally, the new definition of reducibility from formulas to systems of polynomials provides a useful tool for translating formulas into systems of polynomials and studying their relationships.

Link to Article: https://arxiv.org/abs/0308012v1 Authors: arXiv ID: 0308012v1