Is there a way to convince Mathematica to perform quantifier elimination on a semialgebraic set and yield a resulting semialgebraic set whose representation does not involve any roots or radicals, i.e., is given as a Boolean combination of polynomial inequalities? Here is a simple example:

org = Reduce[Exists[{z}, x^2 + 2 x y <= z^3 && x y + z <= 5], {x, y}, Reals]

yields

(x < 0 && y >= Root[-125 + x^2 + 77 x #1 - 15 x^2 #1^2 + x^3 #1^3 &, 1]) || x == 0 ||
(x > 0 && y <= Root[-125 + x^2 + 77 x #1 - 15 x^2 #1^2 + x^3 #1^3 &, 1])

Update: In this specific example, we can use ToRadicals and manually introduce two variables w1, w2 for which the following holds:

cond = w1^3 == Sqrt[3] w2 - 90 x^6 - 9 x^8 &&
w2^2 == 2732 x^12 + 540 x^14 + 27 x^16 &&
w2 >= 0

Substituting these variables for the respective radical expressions yields the following Boolean combination of polynomial inequalities:

new =
((x < 0 && ((6 w1 x^3 y >=
2^(2/3) 3^(1/3) w1^2 + 30 w1 x^2 - 4 2^(1/3) 3^(2/3) x^4 &&
6 w1 x^3 > 0) || (6 w1 x^3 y <=
2^(2/3) 3^(1/3) w1^2 + 30 w1 x^2 - 4 2^(1/3) 3^(2/3) x^4 &&
6 w1 x^3 < 0))) ||
x == 0 ||
(x > 0 && ((6 w1 x^3 y <=
2^(2/3) 3^(1/3) w1^2 + 30 w1 x^2 - 4 2^(1/3) 3^(2/3) x^4 &&
6 w1 x^3 > 0) || (6 w1 x^3 y >=
2^(2/3) 3^(1/3) w1^2 + 30 w1 x^2 - 4 2^(1/3) 3^(2/3) x^4 &&
6 w1 x^3 < 0)))) &&
w1^3 == Sqrt[3] w2 - 90 x^6 - 9 x^8 &&
w2^2 == 2732 x^12 + 540 x^14 + 27 x^16 &&
w2 >= 0

Reduce/Resolve are able to prove the equivalence:

Reduce[ForAll[{x, y, w1, w2}, Implies[cond, Equivalent[org, new]]], {}, Reals]
True

Resolve[ForAll[{x, y}, Exists[{w1, w2}, Equivalent[org, new]]], Reals]
True

However, I wonder about a general solution which should in principle exist.

• What different form might one obtain? Commented Jun 18, 2021 at 14:10
• A Boolean combination of polynomial inequalities p(x) >= 0 (x being a vector here). Commented Jun 18, 2021 at 14:12
• I meant for this specific example. When everything is an equation this is standard variable elimination. But for inequalities it is not clear to me what the result above might be. Commented Jun 18, 2021 at 14:16
• @DanielLichtblau: I extended my post accordingly. However, the approach is not insightful for the general case. Commented Jun 18, 2021 at 15:56
• @MathGaudium: Could you indicate the edited places in your question? Such behavior is standard. Commented Jun 18, 2021 at 16:13