Due to Andreas Blass's answer to my question "Is the feasibility of a system of nonlinear, non-convex equations (inequalities) decidable?", i have now investigated real closed fields (RCF), because i had never studied them before. My background is logic-based cognitive robotics, not model theory or foundations of mathematics. So, the theory of RCF is complete and decidable, but i'm still not sure whether my problem language is a RCF: Literature about RCFs rarely give examples. I would like to know the exact definition of the theory of real numbers which is a RCF. On the Wikipedia page Tarski's axiomatization of the reals, it is mentioned that Tarski showed that the theory of real-closed fields completely axiomatizes the first-order theory of the structure $\langle \mathbb{R}, +, *, < \rangle$.

However, i need to know whether a certain fragment of the first-order logic is decidable, or equivalently, whether a certain class of systems of equations (including the products of at most two variables at a time) is feasible. Is $\langle \mathbb{R}, +, -, *, < \rangle$ (where $\mathbb{R}(x)$ is the predicate stating that $x$ is a real number, or $\mathbb{R}$ is the set of real numbers) a model in the RCF? Is the first order language employed in the theory assumed to include equality (=)? So, do sentences like the following fall within the RCF (assume $x$ and $y$ with subscripts are real number variables)?

$(\exists x_1,x_2,x_3,y_1,y_2,y_3)\quad (x_1*y_2 + x_2*y_3 = 0.223) \; \land$

$\quad \lnot( x_1*y_1 + x_3*y_2 = 0.928) \; \land $

$\quad ((x_1 + x_2 + x_3 = 1) \lor (x_1 + x_2 + x_3 = 0))$.

Moreover, is truth of sentences of this kind decidable and complete in the structure $\langle \mathbb{R}, +, -, *, < \rangle$? Andreas hinted at to the affirmative, but due to my unfamiliarity with the subject, i need to confirm it. I would appreciate a reference which plaintly states that the first-order theory (with =) of real numbers with addition and multiplication is complete and decidable.

Thenyou can “notice” it. @Andreas Thanks for the warning. $\endgroup$ – The User Jun 20 '13 at 18:45