# The decision procedure of theory of closed real field is in NP-hard?

The decision procedure of theory of closed real field refers to https://en.wikipedia.org/wiki/Decidability_of_first-order_theories_of_the_real_numbers

Yes, even in the purely existential case. See https://en.wikipedia.org/wiki/Existential_theory_of_the_reals

• ... and this holds for any first-order theory that admits some model with at least two elements, not just for the real field. – Emil Jeřábek Dec 21 '19 at 7:45
• Sorry, this isn't quite right. If a consistent theory T proves the existence of at least two elements, the existential theory of T is NP-hard. If a theory T is only consistent with the existence of at least two elements, then satisfiability of existential sentences in a model of T is NP-hard, or in other words, the universal theory of T is coNP-hard. – Emil Jeřábek Dec 21 '19 at 11:42