Strength and limitations of Sherali-Adams and Nullstellensatz proof systems

We compare the strength of the algebraic proof systems Sherali-Adams (SA) and Nullstellensatz (NS) with Frege-style proof systems. Unlike bounded-depth Frege, SA has polynomial-size proofs of the pigeonhole principle (PHP). A natural question is whether adding PHP to bounded-depth Frege is enough to simulate SA. We show that SA, with unary integer coefficients, lies strictly between tree-like depth-1 Frege + PHP and tree-like Resolution. We introduce a levelled version of PHP (L PHP) and we show that SA with integer coefficients lies strictly between tree-like depth-1 Frege + L PHP and Resolution. Analogous results are shown for NS using the bijective (i.e. onto and functional) pigeonhole principle and a leveled version of it.