An example on real quantifier elimination
This instructive example has been used by Hoon Hong in a colloquium talk at the University of Passau in 2005.
Let , for given real numbers and .
The graph shows parts of the (x,y)-plane in red where and in blue where . If both inequalities are true, the intersection of the red and blue domains is magenta.
Question: For which and values will be the following statement true?
For all there exists such that and .
The geometrical meaning of this statement is clearly that the magenta domain always has a point for each value, that is, "horizontally infinite".
What positions of the sliders and ensure that the statement is true?