How to understand Tarski’s Real Closed Field theory result

Question

The decision problem I have is: the truth values of any First Order Logic sentences that contain arithmetic operations and equalities/inequalities on any real numbers.

Per Tarski’s Real Closed Field (RCF) theory result, does it mean the above decision problem is decidable?

If not, then in the above decision problem, is it decidable if I replace "any real numbers" with "a subset of real numbers that satisfy the following conditions" ?

The conditions are: This real number subset includes constant 0 and 1 and satisfies the following 3 axioms:

1)the axioms of ordered fields

2)the axiom asserting that every positive number has a square root

3)for every odd number d, the axiom asserting that all polynomials of degree d have at least one root.

I know RCF does not necessarily mean real numbers, but I am trying to use RCF on real numbers.

Answer 1

I'm not sure what you mean by "any real number combined with arithmetic operations and equalities or inequalities are decidable". Do you mean "the set of all real numbers combined with ..."? The short answer is the theorem applies to any subset of real numbers that satisfies those axioms, but it's a much more general result.

Tarski's theorem has little to do with real numbers $\mathbb R$. It's a theorem about formal axiomatic systems, not sets or models.

It states that the first order theory of real closed field is decidable. In other words, given any first order statement (roughly one that allows $\forall, \exists$ and field operations (functions) and order relations), it can be either proved or disproved from the axioms (1)(2)(3) you listed.

By Godel's completeness theorem, this means that every first order statement has the same truth value for all real closed fields. In particular, $\mathbb R$ itself is a real closed field, hence every 1st order statement has a truth value that can be decided from the axioms of (1)-(3) alone, no other fancy ZFC machinery is necessary. Also, all the real algebraic numbers form a real closed field $\mathbb R_{\mathrm{alg}}$, hence it also has decidable first order theory.

It's clear that $\mathbb R$ and $\mathbb R_{\mathrm{alg}}$ are very different, but they can not be distinguished by any first order statement. For example, their cardinalities are different, $\mathbb R$ contains transcendental elements while $\mathbb R_{\mathrm{alg}}$ doesn't. Tarski's theorem implies that in particular cardinality and transcendental elements cannot be characterized by first order statements.

Answer 2

I think there's some confusion here about what decidability of $\mathsf{RCF}$ means.

The theory of real closed fields, $\mathsf{RCF}$, is a theory in first-order logic in the language of ordered rings: $L_{\mathrm{OR}} = \{+,-,\times,0,1,\leq\}$. "$\mathsf{RCF}$ is decidable" means that there is an algorithm (a Turing machine, say) which takes as input an $L_{\mathrm{OR}}$-sentence and returns "yes" or "no" depending on whether $\mathsf{RCF}\vdash \varphi$.

Since $\mathsf{RCF} = \mathrm{Th}(\mathbb{R})$ (which follow from the fact that $\mathbb{R}$ is a real closed field and $\mathsf{RCF}$ is complete), we can interpret a "yes" answer from this algorithm as meaning $\mathbb{R}\models \varphi$ and a "no" answer as meaning $\mathbb{R}\models \lnot \varphi$.

But please note that $L_{\mathrm{OR}}$ cannot talk directly about arbitrary real numbers. Each natural number can be represented by a term of the form $1+1+\dots+1$, but there is no obvious way for $L_{\mathrm{OR}}$ to make statements about $\pi$, for example. Indeed, since there are only finitely many symbols in $L_{\mathrm{OR}}$, there are only countably many $L_{\mathrm{OR}}$-sentences. [And this should not be surprising: countability is necessary to even talk about decidability in the usual sense, since a Turing machine can only accept countably many possible inputs.]

---

However, there is a sense in which the decidability result for $\mathsf{RCF}$ applies to statements about certain real numbers. Say a real number $r$ is definable if there is an $L_{\mathrm{OR}}$-formula $\varphi_r(x)$ in one free variable, such that for all $s\in \mathbb{R}$, $\mathbb{R}\models \varphi_r(s)$ if and only if $s = r$. If $\psi(x_1,\dots,x_n)$ is an $L_{\mathrm{OR}}$-formula with $n$ free variables and $r_1,\dots,r_n$ are definable real numbers, with $r_i$ defined by $\varphi_{r_i}$, then we have $\mathbb{R}\models \varphi(r_1,\dots,r_n)$ if and only if $$\mathbb{R}\models \exists x_1\dots\exists x_n\left(\bigwedge_{i=1}^n \varphi_{r_i}(x_i)\land \psi(x_1,\dots,x_n)\right).$$ So we can decide whether $\mathbb{R}\models \varphi(r_1,\dots,r_n)$ by applying the decision algorithm for $\mathsf{RCF}$ to the sentence above.

It turns out that the definable real numbers are exactly the real algebraic numbers, i.e., those real numbers which are roots to some non-zero polynomial with coefficients in $\mathbb{Q}$. This is a countable real closed subfield of $\mathbb{R}$, the real closure of $\mathbb{Q}$. So it would be reasonable to say that the decision procedure for $\mathsf{RCF}$ applies to $L_{\mathrm{OR}}$-sentences with parameters from the field of real algebraic numbers.