13
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ 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)$. $\endgroup$
    – The User
    Jun 20, 2013 at 13:23
  • $\begingroup$ 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. $\endgroup$ Jun 20, 2013 at 13:47
  • $\begingroup$ 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. $\endgroup$ Jun 20, 2013 at 17:17
  • $\begingroup$ @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. $\endgroup$
    – The User
    Jun 20, 2013 at 18:45

1 Answer 1

23
$\begingroup$

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

$\endgroup$
9
  • $\begingroup$ And yes, I intend that $=$ is in the language, since in model theory it is customarily considered that $=$ is in every language. $\endgroup$ Jun 20, 2013 at 12:25
  • $\begingroup$ 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. $\endgroup$ Jun 20, 2013 at 13:30
  • $\begingroup$ 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/…. $\endgroup$ Jun 21, 2013 at 2:31
  • $\begingroup$ 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. $\endgroup$ Jun 21, 2013 at 2:39
  • 1
    $\begingroup$ @T.... No, this is not correct. Linear Programming is in P, but it is relatively easy to see that 'the quantifier-free fragment of the first order theory of the real numbers is NP-hard: The equations $x_i^2=x_i$ can restrict $x_i$ to 0 or 1, and then a SAT instance can be encoded as a simple non-linear equation system. $\endgroup$ Sep 16, 2019 at 10:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.