## Feasibility via quantifier elimination II

Suppose we want to decide whether the following semialgebraic set

$S := \{(x,y) \in \mathbb{R}^2 \mid x - y^2 + 1 \geq 0 \land -x - y^2 + 1 \geq 0\}$

is nonempty. This is the same as determining whether the following system of polynomial inequalities

$\begin{array}{rrl} g_1 (x, y) :=& x - y^2 + 1 &\geq 0\\ g_2 (x, y) :=& -x - y^2 +1 &\geq 0\end{array}$

is feasible. We now define $S_1 := \{(x,y) \in \mathbb{R}^2 \mid g_1 (x, y) \geq 0\}$, and $S_2 := \{(x,y) \in \mathbb{R}^2 \mid g_2 (x, y) \geq 0\}$. Set $S_1$ is depicted below

and set $S_2$ is depicted below

Note that $S = S_1 \cap S_2$. We depict this intersection below

Visual inspection of the plot of the intersection $S = S_1 \cap S_2$ allows us to conclude that $S$ in nonempty. Asserting that $S$ is nonempty is the same as stating that the proposition

$\exists{x}\exists{y} \left(g_1 (x,y) \geq 0 \land g_2 (x,y) \geq 0\right)$

is true. We can determine the truth value of this proposition via quantifier elimination using the following REDUCE + REDLOG script:

% feasibility via quantifier elimination

rlset ofsf;

% define polynomial functions
g1 :=  x-y^2+1;
g2 := -x-y^2+1;

% define existential formula
phi := ex({x,y}, g1>=0 and g2>=0);

% perform quantifier elimination
rlqe phi;

end;

which produces the truth value true. This means that there exists a $(x,y)$ that satisfies the polynomial inequalities, i.e., $S$ is nonempty.

__________

Remark: the plots in this post were generated by Wolfram Alpha.