# Is the feasibility of a system of nonlinear, non-convex equations (inequalities) decidable?

I would like to know whether the following problem is decidable.

Is the system

$x^T Q_i x + r_i = 0 \mbox{ for } i = 1, ..., k$

$x^T Q_j x + r_j \neq 0 \mbox{ for } j = k+1, ..., t$

feasible, where $x$ is a column vector of length $n$, $x^T$ is the transpose of $x$, $r_i$ and $r_j$ are rational constants in [0,1], and $Q_i$ and $Q_j$ are symmetric indefinite $n \times n$ matrices. Vector $x$ is the $n$ unknowns and they are in [0,1].

According to me (after a series of transformations and added slack variables), the decidability problem above is equivalent to asking whether the global maximum of $q_j^T x$ (a linear term) can be found, subject to non-linear, non-convex quadratic constraints

$x^T Q_i x + q_i^T x + r_i \leq 0 \mbox{ for } i = 1, ..., u$,

where $x$, $r_i$ and $Q_i$ have the same form as before (but are not identical), $q_i$ is a column vector of length $n$, and $q_i^T$ is the transpose of $q_i$.

The latter formulation of the problem can be viewed as a Quadratically Constrained Quadratic Program (QCQP), except that the objective function is linear. And the constraints are, in general, non-linear. Also note that the latter problem is posed as a decision problem, not purely an optimization problem.

Does either one of these problems have a decidability result?

-

For any fixed $n,k,t$, the feasibility question is a first-order formula in the language of real-closed fields; it would have the components of $x$ as existentially quantified variables and the $r$'s and the entries of the $Q$'s as free variables. Tarski's quantifier elimination theorem for real-closed fields converts this to a propositional combination of equations and inequalities for the free variables. The quantifier-elimination is algorithmic. So as long as the components of the $Q$'s are given in such a way that you can algorithmically do arithmetic with them, the feasibility question is decidable.