The strength of multilinear proofs (Q1024659)

The paper is a contribution to the study of proof complexity of algebraic proof systems. The authors introduce a semantic refutation system fMC (formula multilinear calculus) that is similar to the polynomial calculus (PC) except that lines of the proof are represented by multilinear arithmetic formulas. It is shown in the paper that depth-2 fMC simulates PC and resolution, as well as their common generalization PCR (polynomial calculus with resolution), that there are polynomial-size depth-3 fMC refutations over fields of characteristic 0 of the functional pigeonhole principle, and polynomial-size depth-3 fMC refutations over fields including a primitive \(p\)th root of unity of Tseitin mod-\(p\) tautologies. The last two results imply exponential speed-up of fMC over PCR and bounded-depth Frege. A general form of the simulation of PCR by fMC also gives an interesting result that certain proof complexity lower bounds imply circuit lower bounds (namely, any explicit super-polynomial separation between proof systems similar to fMC but operating with general arithmetic circuits, or multilinear circuits, respectively, implies a super-polynomial lower bound on multilinear circuit size of an explicit sequence of multilinear polynomials).