an unquantified Tarski formula

Structure is retained in the output, i.e. no conversion to prenex form or similar is performed. Outer boolean operators are conserved.

$\mathrm{with}\left(\mathrm{QuantifierElimination}\right)\:$$\mathrm{with}\left(\mathrm{QuantifierTools}\right)\:$

$\mathrm{GetUnquantifiedFormula}\left(\mathrm{exists}\left(x\,\mathrm{And}\left(x=0\,\mathrm{exists}\left(y\,y=0\right)\right)\right)\right)$

$x=0\wedge y=0$

The QuantifierElimination:-QuantifierTools:-GetUnquantifiedFormula command was introduced in Maple 2023.

For more information on Maple 2023 changes, see Updates in Maple 2023.