Complexity of Null- and Positivstellensatz proofs Original Research Article

We introduce two versions of proof systems dealing with systems of inequalities: Positivstellensatz refutations and Positivstellensatz calculus. For both systems we prove the lower bounds on degrees and lengths of derivations for the example due to Lazard, Mora and Philippon. These bounds are sharp, as well as they are for the Nullstellensatz refutations and for the polynomial calculus. The bounds demonstrate a gap between the Null- and Positivstellensatz refutations on one hand, and the polynomial calculus and Positivstellensatz calculus on the other.