Given $a$, $b$ and $c$ real numbers, the following statements are equivalent:
- $$\exists x \in \mathbb{R}; ax^2 + bx + c = 0$$
- $$b^2-4ac \geq 0$$
Note that the first statement has a quantifier ($\exists$) while the second one is quantifier free. This is an example of quantifier elimination, a process which I have not studied carefully yet though.
Let $v_1$, $v_2$ and $v_3$ be elements of $S^2$. Consider the statement:
$$ \exists c_1, c_2, c_3 \in \mathbb{R}; c_1^2+c_2^2+c_3^2 = 1 \text{ and } c_1^2v_1 + c_2^2v_2 + c_3^2v_3 = \mathbf{0}.$$
Can one replace such a statement with some quantifier-free statements? If so, is it easy to figure out what they are explicitly?
Edit 1: note that a necessary and sufficient condition for the statement I am interested in to hold is that the kernel of the $3$-by-$3$ matrix $(v_1,v_2,v_3)$ must contain a nonzero vector in the closure of the first octant. Equivalently, a subspace of $\mathbb{R}^3$ (the kernel), a closed cone (the closure of the first octant) and $S^2$ must intersect non-trivially. This is essentially a linear program...
Edit 2: for generic $v_1$, $v_2$ and $v_3$ on $S^2$, the statement I am interested in is equivalent to $\det(v_1,v_2,v_3) = 0$ and either $w_1 \times w_2$ or $-w_1 \times w_2$ belong to the closure of the first octant, where $w_1$ (resp. $w_2$) is the first (resp. second) row of $(v_1,v_2,v_3)$.