Does quantifier elimination help here?

Question

Suppose we have a quantified linear program

$$\exists z_1,\dots,z_{poly(n)}\in\mathbb R$$ $$\exists u_1,\dots,u_n\in\mathcal P\cap\mathbb R^m$$ $$\forall v_1,\dots,v_n\in\mathcal P\cap\mathbb R^m$$ $$AX\leq b$$ where $\mathcal P$ is a bounded and convex polytope defined by $poly(mn)$ inequalities and $X$ is concatenation of all variables.

Then can quantifier elimination help reduce this to a single existential quantifier program with $poly(mn)$ variables and inequalities? Note every defining inequality is of degree $1$.

If $∀$ quantifier had just $\mathbb R^m$ domain then we would even have polynomial time algorithm. So perhaps we can achieve $poly(mn)$ variables and inequalities in general case.

Does something similar to theorem $2$ in http://pages.di.unipi.it/ruggieri/Papers/amai2013.pdf apply here?

Answer 1

Provided $m$, $n$, and the number of inequalities defining $\mathcal P$ are fixed (so that your statement is in first-order logic), quantifier-elimination will provide an equivalent quantifier-free statement, i.e., a Boolean combination of equations and inequalities between polynomials in the entries of $A$, the components of $b$, and the coefficients of the equations defining $\mathcal P$. Unfortunately, the size of that quantifier-free formula can be huge --- doubly exponential in $m$ and $n$, if I remember correctly.

Since you don't insist on quantifier-free but are willing to settle for an existentially quantified statement, the size might not be quite as huge, but I wouldn't be optimistic about doing any better than doubly exponential size.