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
$\begingroup$
$\endgroup$
$\begingroup$
$\endgroup$
Yes, even in the purely existential case. See https://en.wikipedia.org/wiki/Existential_theory_of_the_reals
answered Dec 21 '19 at 7:32
-
2$\begingroup$ ... and this holds for any first-order theory that admits some model with at least two elements, not just for the real field. $\endgroup$ – Emil Jeřábek Dec 21 '19 at 7:45
-
2$\begingroup$ 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. $\endgroup$ – Emil Jeřábek Dec 21 '19 at 11:42
