Effective real Nullstellensatz and variants

We give a constructive proof of the real Nullstellensatz. So we obtain, for every ordered field K, a uniformly primitive recursive algorithm that computes, for the input “a system of generalized signs conditions (gsc) on polynomials of K[X₁, X₂, …, X _n ] impossible to satisfy in the real closure of K, an algebraic identity that makes this impossibility evident. The main idea is to give an “algebraic identity version” of universal and existential axioms of the theory of real closed fields, and of the simplest deduction rules of this theory (as Modus Ponens). We apply this idea to the Hörmander algorithm, which is the conceptually simplest test for the impossibility of a gsc system in the real closure of an ordered field.