Procedure to determine the equality of numbers in rationals plus square root

Question

Consider the set $\mathbb{Q}^\sqrt{}$ of real numbers that can be constructed by applying finitely many of the five operations $+$, $-$, $\cdot$, $/$ and $\sqrt{}$ to a positive rational number. Examples would be $\sqrt{7} - \sqrt{5} - \sqrt{3}$ or $\sqrt{3+\sqrt{2}}-3$.

I would like to find a procedure (an algorithm) which determines of a given number in $\mathbb{Q}^\sqrt{}$ if it is zero or not.

If it is impossible to give such a procedure, I would like to know why.

Answer 1

I've decided to write up my answer given in the comments in details. The main tool I am going to use is decidability of the theory of real closed fields, and the fact $\mathbb R$ is a real closed field. What this means that if we are given a sentence in the first-order language of ordered fields (i.e. using $0,1$, addition, multiplication, inequality and quantifiers over numbers), we can algorithmically decide whether it's true in $\mathbb R$ or not.

That said, it's enough to give a procedure which, given some expression involving $+,-,\cdot,/,\sqrt{}$, will give us a formula which expresses whether it's zero. I will explain this through an example. Take $\sqrt{3+\sqrt{2}}-3$, the example from question.

• $\sqrt{2}$ is defined as $x_1$ satisfying $x_1\cdot x_1=1+1\land x_1>0$.
• $3+\sqrt{2}$ is defined as $x_2$ satisfying $\exists x_1:(x_2=1+1+1+x_1\land(x_1^2=1+1\land x_1>0))$
• $\sqrt{3+\sqrt{2}}$ is defined as $x_3$ satisfying $\exists x_2:\left(\exists x_1:(x_2=1+1+1+x_1\land(x_1^2=1+1\land x_1>0))\land x_3\cdot x_3=x_2\land x_3>0\right)$
• $\sqrt{3+\sqrt{2}}-3$ is defined as $x_4$ satisfying $\exists x_3:\left(\exists x_2:\left(\exists x_1:(x_2=1+1+1+x_1\land(x_1^2=1+1\land x_1>0))\land x_3\cdot x_3=x_2\land x_3>0\right)\land x_3=x_4+1+1+1\right)$
• Finally, $\sqrt{3+\sqrt{2}}-3=0$ is expressed as $\exists x_4:\left(\exists x_3:\left(\exists x_2:\left(\exists x_1:(x_2=1+1+1+x_1\land(x_1^2=1+1\land x_1>0))\\\land x_3\cdot x_3=x_2\land x_3>0\right)\land x_3=x_4+1+1+1\right)\land x_4=0\right)$

I hope the idea here is clear - we inductively give definitions for each subexpression, and then we state the element given by the final definition is equal to zero. It should be clear enough this translation can be done algorithmically, and hence equality of such expressions to zero can be algorithmically decided.

Let me make a quick note on practicality of this algorithm: it's nowhere near practical. Appealing to full decidability of theory of real closed fields is a major overkill. As you can read in the Wikipedia page linked above, the algorithm for deciding full theory is necessarily doubly exponential, so for the formula above, which is about 30 characters long, this would give us a bound on running time which is on the order of $2^{2^{30}}$, which is a number with 300 million digits!

However, the formulas we derive above are not some generic formulas - they are existential, i.e. don't involve any universal quantifiers. For those formulas there is an algorithm with exponential running time - faster, but still impractical, even for small formulas, see here for details.

In conclusion, this gives us that that the problem is solvable in principle. In practice, other algorithms are needed.

Answer 2

The following should work for even for complex $x$. The assumption is that an expression of $x$ of the prescribed form is given, and that there is a sign convention for the root that can be checked algorithmically (see below).

Any given such number $x$ lies in a finite extension field $K$ of $\mathbb Q$. Construct a basis of K and express $x$ in this basis to see whether $x=0$.

OK, so how to construct $K$? That can be done iteratively, following the expression of $x$. Let $K_0=\mathbb Q$, then adjoin roots as needed. In your example then, $K_1=K_0[z_1]/(z_1^2-2)$ and $K_2=K_1[z_2]/(z_2^2-(3 + z_1))$. At this step, one needs to check that $z_2^2-(3 + z_1)$ is irreducible over $K_1$.

In this special case, one simply needs to check whether $y^2-(3 + z_1)$ has a zero $y\in K_1$. This is a system of two quadratic equations in two indeterminates. It is zero-dimensional, since a quadratic equation over the field $K_1$ has at most two solutions. Thus, one can use Gröbner bases with respect to an elimination order to check for a rational solution. (There might be a more elegant algorithm to check irreducibility, but I don't know.)

At last, one checks whether $z_2-3=0$ in $K_2$.

It remains to describe in more detail the reducible case. Suppose that at step $i$ we want to adjoin square root of $p\in K_{i-1}$. If $z_{i}^2-p$ is reducible, then $K_{i-1}$ contains two roots of $p$ (or one of $p=0$). Choose the one that conforms to your sign convention of $\sqrt{}$ and replace $\sqrt{p}$ by this root in the expression of $x$.

So how to single out the correct root? Usually, the square root is defined uniquely by a sign condition on real and imaginary part. I guess there should be a similar iterative algorithm that allows to check such sign conditions. An alternative would be to check this sign condition numerically. Of course, then one might ask: why bother at all, why not just try to answer the original question by numerical evaluation? One reason might be that verifying numerically whether something is zero is extremely difficult, while verifying numerically whether something is positive is relatively easy.