Is the first-order theory (with =) of real numbers with addition and multiplication complete and decidable?

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.

-
An addition to Joel’s nice answer: Notice that you do not need $-, <, 0, 1$ and thet the theory of $(\mathbb{R},+,\cdot)$ is the same as the theory of real algebraic numbers with addition and multiplication, which is the minimal countable elementary substructure of $(\mathbb{R},+,\cdot)$. –  The User Jun 20 '13 at 13:23
The User, is the fact that the real algebraic numbers have the same theory as the reals with addition and multiplication something that you can just "notice", that is, without already knowing Tarski's theorem? I think of this as one of the important consequences of Tarski's theorem, and I would be unsure how to prove it directly, without using Tarski's theorem. –  Joel David Hamkins Jun 20 '13 at 13:47
The User: Cutting down the language to just addition and multiplication is fine for the purposes of the question (about completeness and decidability), but it loses the quantifier-elimination that Joel mentioned in his answer. –  Andreas Blass Jun 20 '13 at 17:17
@Joel No, I would regard that as a consequence of the theorem by Tarski, too. Then you can “notice” it. @Andreas Thanks for the warning. –  The User Jun 20 '13 at 18:45

Yes, all those assertions are expressible in the language of real closed fields, and all such assertions are decidable by Tarski's theorem. You can refer to addition, subtraction, multiplication, division, etc., plus the order; you can refer to any specific rational number (such as .223 etc.) because you have $1$ in the language and can therefore form any rational number; you can form any polynomial and indeed any rational function, with rational coeffficients, in any specific finite number of variables; and you can quantify over the real numbers and apply any kind of logical connective.

What Tarski proved is that in fact every such assertion is equivalent to a (much longer) quantifier-free assertion, and this is ultimately why they are decidable.

Theorem. (Tarski) The first-order theory of real-closed fields, which is the same as the theory of the structure $\langle\mathbb{R},+,\cdot,0,1,\lt\rangle$ is complete and decidable, and admits quantifier-elimination.

What you cannot do while remaining under the decidability result is quantify over the integers or the rational numbers. So you cannot necessarily decide questions like, "does this specific polynomial $p(\vec x)$ have an integer solution?". In particular, if you add a predicate for the integers to the structure, forming $\langle\mathbb{R},+,\cdot,\mathbb{Z},0,1,\lt\rangle$, where $\mathbb{Z}$ is a predicate that is true of exactly the real numbers that are integers, then the theory is no longer decidable. For this reason, the theory of the structure $\langle\mathbb{R},+,\cdot,\sin(x),0,1,\lt\rangle$ is not decidable, because in it we can define the integers. So while you can refer to specific polynomial or rational functions over the integers, you may not quantify over the class of such polynomials.

Similarly, you also cannot quantify over the dimension (which amounts to an integer quantifier), and ask something like: does every upper triangular $n\times n$ matrix (for every $n\geq 1$) have a certain property? That is, in order to stay within Tarski's language, you can in effect quantify over $\mathbb{R}^3$ or $\mathbb{R}^{86}$ or $\mathbb{R}^n$ for a specific $n$ by using $n$ individual real quantifiers, but you cannot treat $n$ itself as a variable here.

My opinion---probably overblown---is that Tarski's theorem is one of the great pinnacles of mathematical achievement. One of the consequences of his theorem, for example, is that Cartesian geometry is decidable. Tarski's theorem provides an algorithm that will decide by rote any question you can put to it about lines, circles, ellipses, cones, spheres, ellisoids, planes, cubes and so on, in any specific dimension. All such questions are expressible in the language of real-closed fields. (OK, I admit that the algorithm takes double exponential time, and is not feasible. But still, I find the existence of such an algorithm for a topic that has been studied by mathematicians for thousands of years to be amazing.)

-
And yes, I intend that $=$ is in the language, since in model theory it is customarily considered that $=$ is in every language. –  Joel David Hamkins Jun 20 '13 at 12:25
And in line with The User's comment above, you can also refer to any specific real algebraic number, since these are all definable. So you can have polynomials and rational functions with coefficients like $\sqrt{3+\sqrt{2}}$ and so on, using any algebraic number. –  Joel David Hamkins Jun 20 '13 at 13:30
Joel - I've very interested in collecting examples (such as are definitively known) of algebraic theorem schemata in which your dimension'' parameter $n$ may itself be formally quantified, after due coding and translation into, say, Peano Arithmetic: see mathoverflow.net/questions/105478/…. –  Adam Epstein Jun 21 '13 at 2:31
My real motivation is that the fundamental rigidity theorem (due to Thurston) in 1 dimensional holomorphic dynamics is an extremely natural example for which there is a transcendental proof, but for which no general algebraic proof is known. The statement can be readily coded into PA. Surely a true mathematical incompleteness in PA cannot be obtained so cheaply...and yet we have no explicit understanding of the algebraic number theory involved. –  Adam Epstein Jun 21 '13 at 2:39
I want to heartly thank you and Andreas for your answers. This might me the last major hurdle overcome in my PhD research! As you said, Joel, Tarski's theorem is powerful, and until Andreas's answer, i actually suspected that my problem was undecidable: Consider, e.g., optimization algorithms for quadratically constrained quadratic programs (QCQPs); they can tell whether a system of (nonlinear) equations is feasible only with $\epsilon$-tolerance, that is, only to within so-called `mathematical certainty'. It is strange that none of the literature about nonlinear programming mention Tarski –  Gavin Jun 22 '13 at 11:40