Can one always Decide whether a Systems of Nonlinear Equations with Bilinear terms is Feasible?

Question

I have come to a point in my PhD research were i need to prove that a particular decision procedure is decidable or not. And if i can solve the sub-problem described below, i shall have proved it. The problem description follows, and then i state my main question.

I have tried to give an example which illustrates the main features of the kind of problem i am dealing with. Giving the problem in general form would be too complicated for the reader.

Let $\alpha_{j}, \beta_{k} \in \mathbb{R}$ be the variables of the problem. Auxiliary variables $y_1,y_2 \in \mathbb{R}$ were added in a preprocessing step. The problem will never have coefficients. Terms will `at worst' be bilinear.

$\alpha_{1} + \alpha_{2} + \alpha_{3} + \alpha_{4} = 1$

$\alpha_{1} + \alpha_{2} = 0.5$

$\alpha_{2} + \alpha_{4} = 0.6$

$\beta_{1} + \beta_{2} = 1$

$\beta_{3} + \beta_{4} = 1$

$\beta_{5} + \beta_{6} = 1$

$\beta_{7} + \beta_{8} = 1$

$\alpha_{1}\beta_{1} + \alpha_{2}\beta_{3} = 0.1$

$\alpha_{2}\beta_{4} + \alpha_{4}\beta_{8} = 0.4$

$-\alpha_{2}\beta_{3} + y_1 \leq -0.7$

$\alpha_{4}\beta_{8} + y_2 \leq 0.33$

$y_1,y_2>0$

$0\leq \alpha_{j} , \beta_{k} \leq 1, \mbox{ for } j =1,2,3,4, k=1,2,\ldots,8.$

Note that this is not an optimization problem. I do not even necessarily want a solution; all i want to know is whether there exists a feasible solution to the system or not.

My question is, Is there a theorem or can one prove that a nonlinear system of equations and inequalities with linear and bilinear terms (as sketched above) is decidable or undecidable w.r.t. the existence of a feasible solution?

In fact, it is preferred that $\alpha_{j}, \beta_{k}, y_1,y_2 \in \mathbb{Q}$, the rational numbers. But if results are known only for variables in the real numbers, then it would be very helpful.

I would greatly appreciate your comments on this question.

Answer 1

Over the reals, this sort of question is decidable, because it's in the first-order theory of the real field, which is decidable by an old theorem of Tarski. Over the rationals, this is as hard as the general question of solvability of Diophantine equations. The point is that, even if a Diophantine equation involves products of more than two variables, it's equivalent to a system in which additional variables are introduced for sub-products, and these can be defined by quadratic equations. And quadratic expressions that aren't bilinear, like $x^2$, can be replaced by $xy$ where $y$ is fresh variable and the equation $x=y$ is added to the system.