PROOF COMPLEXITY IN ALGEBRAIC SYSTEMS AND BOUNDED DEPTH FREGE SYSTEMSWITH MODULAR COUNTING

We prove a lower bound of the form N-Ohm(1) on the degree of polynomia ls in a Nullstellensatz refutation of the Count(q) polynomials over Z( m), where q is a prime not dividing m. In addition, we give an explici t construction of a degree N-Ohm(1) design for the Count(q) principle over Z(m). As a corollary, using Beame et al. (1994) we obtain a lower bound of the form 2(N Ohm(1)) for the number of formulas in a constan t-depth Frege proof of the modular counting principle Count(q)(N) from instances of the counting principle Count(m)(M). We discuss the polyn omial calculus proof system and give a method of converting tree-like polynomial calculus derivations into low degree Nullstellensatz deriva tions. Further we show that a lower bound for proofs in a bounded dept h Frege system in the language with the modular counting connective MO Dp follows from a lower bound on the degree of Nullstellensatz proofs with a constant number of levels of extension axioms, where the extens ion axioms comprise a formalization of the approximation method of Raz borov (1987) and Smolensky (1987) (in fact, these two proof systems ar e basically equivalent).