1
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ What different form might one obtain? $\endgroup$ Jun 18, 2021 at 14:10
  • $\begingroup$ A Boolean combination of polynomial inequalities p(x) >= 0 (x being a vector here). $\endgroup$ Jun 18, 2021 at 14:12
  • $\begingroup$ 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. $\endgroup$ Jun 18, 2021 at 14:16
  • $\begingroup$ @DanielLichtblau: I extended my post accordingly. However, the approach is not insightful for the general case. $\endgroup$ Jun 18, 2021 at 15:56
  • 2
    $\begingroup$ @MathGaudium: Could you indicate the edited places in your question? Such behavior is standard. $\endgroup$
    – user64494
    Jun 18, 2021 at 16:13

1 Answer 1

1
$\begingroup$

Yes, there is such away:

ToRadicals[Root[-125 + x^2 + 77 x #1 - 15 x^2 #1^2 + x^3 #1^3 &, 1], Assumptions -> x < 0]

5/x - (2 (2/3)^( 1/3) x)/(-90 x^6 - 9 x^8 + Sqrt[3] Sqrt[2732 x^12 + 540 x^14 + 27 x^16])^( 1/3) + (-90 x^6 - 9 x^8 + Sqrt[3] Sqrt[2732 x^12 + 540 x^14 + 27 x^16])^(1/3)/( 2^(1/3) 3^(2/3) x^3)

ToRadicals[Root[-125 + x^2 + 77 x #1 - 15 x^2 #1^2 + x^3 #1^3 &, 1], Assumptions -> x > 0]

5/x - (2 (2/3)^( 1/3) x)/(-90 x^6 - 9 x^8 + Sqrt[3] Sqrt[2732 x^12 + 540 x^14 + 27 x^16])^( 1/3) + (-90 x^6 - 9 x^8 + Sqrt[3] Sqrt[2732 x^12 + 540 x^14 + 27 x^16])^(1/3)/( 2^(1/3) 3^(2/3) x^3)

$\endgroup$
1
  • $\begingroup$ Thank you. I also extended my post with a manually constructed solution that involves two additional variables. However, I wonder how this can be done in general with Mathematica without relying on ToRadicals which cannot be used for in general. It should be possible though because a semialgebraic set can always be represented as a Boolean combination of polynomial inequalities. $\endgroup$ Jun 18, 2021 at 15:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.