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.