The Strength of Multilinear Proofs

. We introduce an algebraic proof system that manipulates multilinear arithmetic formulas. We show that this proof system is fairly strong, even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, we show the following: Algebraic proofs manipulating depth 2 multilinear arithmetic formulas polynomially simulate Resolution, Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR) proofs; Polynomial size proofs manipulating depth 3 multilinear arithmetic formulas for the functional pigeonhole principle; Polynomial size proofs manipulating depth 3 multilinear arithmetic formulas for Tseitin’s graph tautologies. By known lower bounds, this demonstrates that algebraic proof systems manipulating depth 3 multilinear formulas are strictly stronger than Resolution, PC and PCR, and have an exponential gap over bounded-depth Frege for both the functional pigeonhole principle and Tseitin’s graph tautologies. We also illustrate a connection between lower bounds on multilinear proofs and lower bounds on multilinear circuits. In particular, we show that (an explicit) super-polynomial size separation between proofs manipulating general arithmetic circuits and proofs manipulating multilinear circuits implies a super-polynomial size lower bound on multilinear circuits for an explicit family of polynomials.