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.
Best Answer
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.)